Określanie typu funkcji w Programowaniu funkcjonalnym

Question

Następujące równania są napisane w składni Miranda, ale ze względu na podobieństwa między Mirandą i Haskellem oczekuję, że programiści Haskell powinni to zrozumieć!

Jeśli zdefiniować następujące funkcje:

rc v g i = g (v:i) 
rn x = x 
rh g = hd (g []) 


f [] y = y 
f (x:xs) y = f xs (rc x y) 

g [] y = y 
g (x:xs) y = g xs (x:y) 

Jak wypracować rodzaj funkcji? Myślę, że rozumiem, jak to zrobić dla f, g i rn, ale jestem zdezorientowany z częściowej części aplikacji.

rn będzie * -> * (lub cokolwiek -> coś, myślę, że jest to -> a w Haskell)

dla F i G są rodzaje funkcji zarówno [*] -> * -> *?

Nie jestem pewien, jak podejść do wyszukiwania typów dla rc i rh. W rc, g jest częściowo stosowane do zmiennej i - więc domyślam się, że ogranicza to typ i do [*]. Jaka jest kolejność rc i g w definicji rc? Czy g stosuje się do i, a następnie wynikowa funkcja używana jako argument dla rc? Czy też rc pobiera 3 oddzielne parametry v, gi i? Jestem naprawdę zdezorientowany .. każda pomoc byłaby doceniona! Dzięki chłopaki.

Niestety zapomniał dodać, że HD to standardowa funkcja głowa na liście i jest zdefiniowany jako:

hd :: [*] -> * 
hd (a:x) = a 
hd [] = error "hd []" 

Answer 1

Typ jest wywnioskować z tego, co jest już znane od rodzaju i sposobu wyrażenia są używane w definicji.

Zacznijmy od góry,

rc v g i = g (v : i) 

tak rc :: a -> b -> c -> d i musimy zobaczyć, co można znaleźć na temat a, b, c i d. Po prawej stronie pojawia się (v : i), więc przy v :: a widzimy, że i :: [a], c = [a]. Następnie g nakłada się v : i, więc g :: [a] -> d, zupełnie,

rc :: a -> ([a] -> d) -> [a] -> d 

rn x = x oznacza, że ​​nie ma ograniczenia typu argument rn i jego typ zwracany jest taki sam, rn :: a -> a.

rh g = hd (g []) 

Od rh argumentacja g jest stosowana do pustej listy na RHS, musi mieć typ [a] -> b, ewentualnie więcej informacji na temat a lub b następująco. Rzeczywiście, g [] jest argument hd na RHS, więc g [] :: [c] i g :: [a] -> [c], stąd

rh :: ([a] -> [c]) -> c 

Następny

f [] y = y 
f (x:xs) y = f xs (rc x y) 

Pierwszym argumentem jest lista, a jeśli to jest puste, to wynik jest drugi argument, więc f :: [a] -> b -> b wynika z pierwszego równania.Teraz, w drugim równaniu, na RHS, drugim argumentem na f jest rc x y, a więc musi być tego samego typu co y, nazwaliśmy to b. Ale

, czyli b = [a] -> d. Stąd

f :: [a] -> ([a] -> d) -> [a] -> d 

Wreszcie

g [] y = y 
g (x:xs) y = g xs (x:y) 

z pierwszego równania wywnioskować g :: [a] -> b -> b. Z drugiego, możemy wywnioskować b = [a], ponieważ bierzemy głowę pierwszego argumentu i minusy go g „s na sekundę, co

g :: [a] -> [a] -> [a] 

Answer 2

Zamierzam użyć składni Haskell napisać typy.

rc v g i = g (v:i) 

Tutaj rc przyjmuje trzy parametry, więc jej typ będzie coś a -> b -> c -> d. v:i musi być listą elementów tego samego typu, co v i i, czyli v :: a i i :: [a]. g jest stosowana do tej listy, tak aby g :: [a] -> d. Jeśli umieścisz wszystko razem, otrzymasz rc :: a -> ([a] -> d) -> [a] -> d.

Jak już ustaliłeś, rn :: a -> a, ponieważ jest to po prostu tożsamość.

Nie mam pojęcia o typie funkcji hd, której używasz w rh, więc pominę to.

f [] y = y 
f (x:xs) y = f xs (rc x y) 

Tutaj f przyjmuje dwa parametry, więc jej typ będzie coś a -> b -> c. Od pierwszego przypadku możemy wywnioskować, że b == c, ponieważ zwracamy y, i że pierwszym argumentem jest lista. Teraz wiemy, że f :: [a'] -> b -> b. W drugim przypadku wypowiedzenia jak x i y są podane na wejściu do rc: y musi być funkcją [a'] -> d i rc x y :: a' -> d (które muszą być również rodzaj y, ponieważ jest ona przekazywana jako to drugi argument f). Wreszcie możemy powiedzieć, że f :: [a'] -> ([a'] -> d) -> ([a'] -> d). Ponieważ -> jest prawostronny, jest to równoważne z [a'] -> ([a'] -> d) -> [a'] -> d.

Możesz rozumować w ten sam sposób w odniesieniu do pozostałych.