Funkcja ML typu „a ->” b

Nasz profesor poprosił nas o przemyślenie funkcji w OCaml, która ma ten typ

'a -> 'b

tj. funkcja jednego argumentu, który może być czymkolwiek, i który może zwrócić coś innego.

Myślałem o użyciu raisefunkcji, która ignoruje jej argument:

let f x = raise Exit

Ale profesor powiedział, że istnieje rozwiązanie, które nie wymaga żadnej funkcji w standardowej bibliotece. Jestem zdezorientowany: jak możesz to zrobić, 'bjeśli go nie masz?

_{Pytam tutaj, a nie na temat Przepełnienia stosu, ponieważ chcę zrozumieć, co się dzieje, nie chcę po prostu zobaczyć programu bez wyjaśnienia.}

Szkielet jest let f x = BODY. W BODY musisz używać x tylko w sposób ogólny (na przykład nie wysyłaj go do funkcji, która oczekuje liczb całkowitych) i musisz zwrócić wartość dowolnego innego typu. Ale jak ta ostatnia część może być prawdziwa? Jedynym sposobem spełnienia instrukcji „dla wszystkich typów 'b, zwracana wartość jest wartość typu 'b”, to upewnienie się, że funkcja nie zwróci. Istnieją dokładnie dwie możliwości: usterka BODY lub nie kończy się. Funkcja raisepowoduje błąd, następujące nie kończą się:

let rec f x = f x

Najpierw kilka uwag. Używając tylko podstawowego rachunku lambda nie można uzyskać, 'a -> 'bponieważ system pisania jest zgodny (poprzez izomorfizm Curry'ego Howarda ) z logiką intuicyjną, a odpowiadająca mu formuła A → Bnie jest tautologią.

Inne rozszerzenia, takie jak krotki i dopasowania / warunkowe, nadal zachowują pewną logiczną spójność, dodając typy produktów, *które odpowiadają logicznemu łącznikowi i , i typy sum, |które odpowiadają or . Ponownie, nie oczekuj, że wyprodukują taki 'a -> 'btyp, ponieważ pozwoliłoby to udowodnić jakąś formułę, która nie jest tautologią.

Zatem jedynymi szansami są inne konstrukcje, które wymykają się logice, takie jak raise(ale w tym przypadku nie możesz)… lub let rec! Rekurencja pozwala budować programy, które nigdy się nie kończą, a ich wyniki mogą otrzymać dowolny typ zwrotu, ponieważ nigdy nie zostaną wyprodukowane. Teraz, jeśli pomyślisz o najbardziej trywialnej nie kończącej się funkcji (tej, która bezpośrednio wywołuje się, aby zwrócić wynik):

let rec f x = f x

Zauważysz, że jego typ jest dokładnie taki 'a -> 'b: niezależnie od podanego argumentu, można założyć, że wynik (który nigdy nie zostanie obliczony) może mieć dowolny typ.

Oczywiście fnie jest to interesująca funkcja, ale o to właśnie chodzi. W OCaml każda funkcja, której typ nie wygląda na prawidłową formułę, jest funkcją podejrzaną.

Używając prymitywów kompilatora możesz napisać to:

external magic: 'a -> 'b = "%identity"

(i rzeczywiście zapewnia to kompilator, choć nie jest to część języka). To jest niebezpieczna obsada tożsamości.

Twój profesor prawie na pewno tego nie chce. Jest to jednak jedyna przydatna funkcja z typem, o 'a -> 'bktórej wiem i faktycznie jest używana w samej dystrybucji OCaml.