Dlaczego moja definicja typu została odrzucona jako cykliczna, gdy została zadeklarowana jako odmiana, ale zaakceptowana w inny sposób? - typy, funkcjonalne programowanie, ocaml, ml, cykliczne

Miałem problemy z używaniem OCaml do implementacji niektórych struktur danych w czysto funkcjonalnych strukturach danych Chrisa Okasaki i natknąłem się na tę definicję typu:

 type tree = Node of int * int * tree list;;

Nie sądziłem, że potrzebuje tagu, ponieważ nie był to typ unii, więc próbowałem usunąć znacznik, jednak wystąpił następujący błąd:

# type tree = int * int * tree list;;
Characters 5-33:
type tree = int * int * tree list;;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The type abbreviation tree is cyclic

Dlaczego tak się dzieje w przypadku dwóch pozornie równoważnych definicji typów?

Odpowiedzi:

8 dla odpowiedzi № 1

W językach podobnych do ML definicja definicjityp rekurencyjny to taki, w którym rekurencja nie przechodzi przez typ wariantowy. Jest to pragmatyczna definicja w tym sensie, że prowadzi do bardziej użytecznego sprawdzenia typu.

Nie ma nic trudnego w rekurencyjnych typach. Możesz włączyć obsługę typów rekurencyjnych w OCaml z -rectypes flaga.

$ ocaml -rectypes
OCaml version 4.02.1

# type tree = int * int * tree list;;
type tree = int * int * tree list
# let x: tree = (3, 3, [(4, 4, [])]);;
val x : tree = (3, 3, [(4, 4, [])])

Wszystkie typowe silne gwarancje na pisanie sąobecny, gdy włączone są typy rekursywne. Główną wadą jest to, że wiele niezamierzonych programów jest akceptowanych. Innymi słowy, obecność typu rekurencyjnego jest często oznaką błędu programowania.

---

1 dla odpowiedzi nr 2

Pierwsza definicja typu definiuje nowy typ. Gdy pominiesz nazwę konstruktora, zamiast definiować nowy typ, faktycznie wprowadzisz skrót typu, a domyślnie skróty typu nie mogą być rekursywne, ponieważ zazwyczaj nie jest to to, co masz na myśli.

Można użyć dowolnej składni definicji typu, która definiuje nowy typ, aby tworzyć typy rekurencyjne, a nie tylko warianty. Na przykład rekordy będą działać

type tree = { node : int * int * tree list }

lub nawet lepiej

type tree = {
value : int;
depth : int;
children : tree list;
}

(uwaga: nazwy pól zostały wybrane arbitralnie, ponieważ nie znam ich pierwotnego celu)

Podsumowując, typy sum są używane nie tylko do wprowadzania rozłącznych zbiorów typów, ale także do tworzenia nowych typów, a więc:

 type t = Constr x

wprowadza typ t, który można skonstruować za pomocą konstruktora Constr od wartości typu x.

---