Mylące o wnioskach typu Haskell

Question

Właśnie zacząłem uczyć się Haskella. Haskell, jak jest podane statycznych i typ polimorficzne wnioskowanie, typu funkcji tożsamości jest

id :: a -> a 

wskazuje identyfikator może mieć dowolny typ jako parametr i zwraca się. To działa dobrze, gdy próbuję:

a = (id 1, id True) 

po prostu założyć, że w czasie kompilacji, pierwszy id jest Num A :: a -> a, a druga id jest Bool -> Bool. Kiedy próbuję następujący kod, daje błąd:

foo f a b = (f a, f b) 
result = foo id 1 True 

pokazuje typ musi być tego samego typu B, ponieważ współpracuje z

result = foo id 1 2 

Ale czy to prawda, że typ parametru id może być polimorficzny, więc aib mogą być innego typu?

Answer 1

Dobra, to dziwny, upiorny zakątek systemu typu Haskella. Problem polega na tym, że istnieją dwa sposoby wpisywania wnioskowania do funkcji foo.

-- rank 1 
foo :: forall a b. (a -> b) -> a -> a -> (b, b) 
foo f a b = (f a, f b) 

-- rank 2 
foo' :: (forall a. a -> a) -> a -> b -> (a, b) 
foo' f a b = (f a, f b) 

Drugi typ to ten, który chcesz, ale pierwszy typ to ten, który otrzymujesz. Drugi typ, jak zauważył Amalloy, jest typem drugiego rzędu (będziemy ignorować to, co te dwa oznacza, ale przeczytaj wprowadzenie w "Practical type inference for arbitrary-rank types", jeśli chcesz dobrze wyjaśnić rangi - nie zniechęcaj się akademickim charakter pliku PDF na początku jest dostępny i wyraźnie napisany).

Odłożymy na razie definicję typów wyższej rangi i stwierdzimy, że problem polega na tym, że GHC nie może wywnioskować typu rangi 2. Zacytuj papier:

Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code....

Kfoury and Wells show that typeability is decidable for rank ≤ 2, and undecidable for all ranks ≥ 3 (Kfoury & Wells, 1994). For the rank-2 fragment, the same paper gives a type inference algorithm. This inference algorithm is somewhat subtle, does not interact well with user-supplied type annotations, and has not, to our knowledge, been implemented in a production compiler.

Niezdecydowany oznacza, że ​​nie może istnieć żaden algorytm, który zawsze prowadzi do prawidłowej decyzji tak lub nie. Tak więc masz to: niemożliwe do określenia typ rangi 3 lub wyższego i zbyt trudno jest wywnioskować typ rangi 2.

Teraz z powrotem do rangi 2. W przypadku (forall a. a -> a) jest to ranga 2. There's already an excellent Stack Overflow question about what the forall keyword means więc będę odnosić się do tego, ale w zasadzie oznacza to, że jesteś w stanie wywołać f a i f b w wyrażeniu (f a, f b) podczas mający a i b być różne rodzaje, czyli to, czego chciał w pierwszej kolejności, przed wszystkimi ten gorący bałagan.

Jedna ostatnia rzecz: powodem, dla którego normalnie nie widzisz forall s w GHCi jest to, że wszystkie forall s na bardzo zewnętrznym zasięgu są wyłączone. Tak więc forall a b. (a -> b) -> a -> a -> (b, b) jest odpowiednikiem (a -> b) -> a -> a -> (b, b).

Ogólnie rzecz biorąc jest to trudny język, który jest źle wyjaśniony.

(Cynk kapelusza do @amalloy w komentarzach.)