typu podpis combinator nie pasuje do podpisu wpisz jego odpowiednik funkcji Lambda

Question

Rozważmy COMBINATOR:

S (S K) 

zastosować go do argumentów XY:

S (S K) X Y 

kurczy się:

X Y 

Przekonwertowałem S (SK) na odpowiednie warunki lambda i otrzymałem wynik:

(\x y -> x y) 

użyłem funkcji Haskell WinGHCi uzyskać podpis wpisz o (\ X Y -> X Y) i powrócił:

(t1 -> t) -> t1 -> t 

Ma to sens dla mnie.

Następnie użyłem WinGHCi uzyskać podpis typu S (s k) i powrócił:

((t -> t1) -> t) -> (t -> t1) -> t 

To nie ma dla mnie sensu. Dlaczego podpisy typów są różne?

Uwaga: I zdefiniowane s, k, a ja jak:

s = (\f g x -> f x (g x)) 
k = (\a x -> a) 
i = (\f -> f) 

Answer 1

Dziękuję wszystkim, którzy odpowiedzieli na moje pytanie. Przestudiowałem twoje odpowiedzi. Aby upewnić się, że rozumiem to, czego się nauczyłem, napisałem własną odpowiedź na moje pytanie. Jeśli moja odpowiedź jest nieprawidłowa, proszę dać mi znać.

Zaczynamy rodzajów k i s:

k :: t1 -> t2 -> t1 
    k = (\a x -> a) 

    s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
    s = (\f g x -> f x (g x)) 

Niech najpierw pracę na określanie typu podpis z (s k). 'Definicja s:

s = (\f g x -> f x (g x)) 

Podstawiając k dla f wyniki (\f g x -> f x (g x)) zamawiającym:

(\g x -> k x (g x)) 

Ważne Rodzaj gi X musi być zgodna z k'

Przypomnijmy s s wpisz podpis.

Przypomnijmy, że k ma tego typu podpis:

k :: t1 -> t2 -> t1 

Tak więc, w tym definicji funkcji k x (g x) możemy wnioskować:

• Rodzaj x jest typem pierwszego argumentu k „s , który jest typu t1.

• typu drugiego argumentu k jest to t2, dzięki czemu wynik może być (g x)t2.

• g ma x jako argument, który już określiliśmy, ma typ t1. Tak więc sygnatura typu (g x) to (t1 -> t2).

• typ wyniku k jest to t1, więc skutkiem (s k) jest t1.

Więc podpis rodzaj (\g x -> k x (g x)) to:

(t1 -> t2) -> t1 -> t1 

Następnie k jest zdefiniowana zawsze powrócić swój pierwszy argument.Więc tak:

k x (g x) 

kontrakty do tego:

x 

I tak:

(\g x -> k x (g x)) 

kontrakty na to:

(\g x -> x) 

Ok, teraz zorientowali się (s k) :

s k :: (t1 -> t2) -> t1 -> t1 
    s k = (\g x -> x) 

Teraz określmy typ podpisu s (s k).

Postępujemy w ten sam sposób. 'Definicja s:

s = (\f g x -> f x (g x)) 

Podstawiając (s k) dla f wyniki (\f g x -> f x (g x)) zamawiającym:

(\g x -> (s k) x (g x)) 

Ważne Rodzaj g i x muszą być zgodne z (s k)'

Przypomnijmy s s wpisz podpis.

Przypomnijmy, że (s k) ma tego typu podpis:

s k :: (t1 -> t2) -> t1 -> t1 

Tak więc, w tym definicji funkcji (s k) x (g x) możemy wnioskować:

• Rodzaj x jest typem pierwszego argumentu (s k) „s , który jest typu (t1 -> t2).

• typu drugiego argumentu (s k) jest to t1, dzięki czemu wynik może być (g x)t1.

• g ma x jako argument, który już określiliśmy ma typ (t1 -> t2). Zatem sygnatura typu (g x) to ((t1 -> t2) -> t1).

• typ wyniku (s k) jest to t1, więc skutkiem s (s k) jest t1.

Więc podpis rodzaj (\g x -> (s k) x (g x)) to:

((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Wcześniej ustaliliśmy, że s k ma taką definicję:

(\g x -> x) 

Oznacza to, że jest to funkcja, która trwa dwa argumentuje i zwraca drugi.

W związku z tym:

(s k) x (g x) 

kontrakty na to:

(g x) 

I tak:

(\g x -> (s k) x (g x)) 

kontrakty na to:

(\g x -> g x) 

Okay, teraz ustaliliśmy, s (s k).

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
    s (s k) = (\g x -> g x) 

Wreszcie porównać podpis typu z s (s k) z podpisem typu tej funkcji:

p = (\g x -> g x) 

Rodzaj p jest:

p :: (t1 -> t) -> t1 -> t 

p i s (s k) mają taką samą definicję (\g x -> g x) dlaczego więc mają różne podpisy typów?

Powodem, dla którego s (s k) ma inny podpis niż p jest to, że nie ma ograniczeń na p. Widzieliśmy, że s w (s k) jest ograniczony do sygnatury typu k, a pierwsza s w s (s k) jest ograniczona, aby była zgodna z sygnaturą typu (s k). Tak więc podpis typu s (s k) jest ograniczony ze względu na jego argument. Chociaż p i s (s k) mają taką samą definicję, ograniczenia na g i x różnią się.

Answer 2

Zaczynamy rodzajów k i s

k :: t1 -> t2 -> t1 
k = (\a x -> a) 

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
s = (\f g x -> f x (g x)) 

Więc przechodząc k jako pierwszy argument s, my Ujednolicenie typu k z rodzajem pierwszego argumentu o numerze s i użycie s dla typu

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1 

Stąd uzyskania

s k :: (t1 -> t2) -> t1 -> t1 
s k = (\g x -> k x (g x)) = (\g x -> x) 

Następnie w s (s k) zewnętrzna s stosuje się typ (t3 = t1 -> t2, t4 = t5 = t1)

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

zastosowaniem tego celu s k spada typ pierwszego argumentu i zostawia nas pod numerem

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Podsumowując: w języku Haskell typ s (s k) pochodzi od typów jego podwyrażeń składowych, a nie od jego wpływu na jego argumenty. Dlatego ma mniej ogólny typ niż wyrażenie lambda, które oznacza efekt s (s k).

Answer 3

System typów, którego używasz, jest w zasadzie taki sam jak prosty typ lambda (nie używasz żadnych funkcji rekursywnych lub rekursywnych). Prosty rachunek lambda nie jest w pełni ogólny; nie jest to Turing-complete i nie można go użyć do napisania ogólnej rekurencji.Kombinator kombinacyjny SKI jest Turing-complete i może być używany do pisania kombinatorów stałych i ogólnej rekursji; w związku z tym pełna moc rachunku kombinatorycznego SKI nie może być wyrażona w prostym typie rachunku lambda (chociaż może być w nieoptymowanym rachunku lambda).