Zaczynam rozumieć, w jaki sposób forallsłowo kluczowe jest używane w tak zwanych „typach egzystencjalnych”, takich jak:

data ShowBox = forall s. Show s => SB s

Jest to jednak tylko podzbiór tego, w jaki sposób foralljest używany i po prostu nie mogę skupić się na jego użyciu w takich rzeczach:

runST :: forall a. (forall s. ST s a) -> a

Lub wyjaśnienie, dlaczego są one różne:

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Lub cała RankNTypessprawa ...

Wolę raczej czysty, pozbawiony żargonu angielski niż te, które są normalne w środowisku akademickim. Większość wyjaśnień na ten temat (które mogę znaleźć w wyszukiwarkach) ma następujące problemy:

1. Są niekompletne. Wyjaśniają, jedną część używania tego słowa kluczowego (na przykład „typów egzystencjalnych”), co sprawia, że czuję się szczęśliwy, dopóki nie przeczytałem kod, który używa go w zupełnie inny sposób (jak runST, fooi barpowyżej).
2. Są gęsto wypełnione założeniami, że czytałem najnowsze w jakiejkolwiek gałęzi dyskretnej matematyki, teorii kategorii lub algebry abstrakcyjnej, która jest popularna w tym tygodniu. (Jeśli nie czytam słowa „konsultować papier co do szczegółów realizacji” ponownie, będzie to zbyt szybko).
3. Są napisane w sposób, który często zamienia nawet proste pojęcia w kręto pokręconą i złamaną gramatykę i semantykę.

Więc...

Przejdź do właściwego pytania. Czy ktoś może całkowicie wyjaśnić forallsłowo kluczowe w jasnym, prostym języku angielskim (lub, jeśli istnieje, wskazać tak jasne wyjaśnienie, którego mi brakowało), które nie zakłada, że ​​jestem matematykiem pogrążonym w żargonie?

Edytowano, aby dodać:

Poniżej były dwie wyróżniające się odpowiedzi spośród tych o wyższej jakości, ale niestety mogę wybrać tylko jedną najlepszą. Odpowiedź Normana była szczegółowa i użyteczna, wyjaśniając rzeczy w sposób, który pokazał niektóre teoretyczne podstawy, foralla jednocześnie pokazując niektóre praktyczne implikacje tego. odpowiedź yairchuobejmował obszar, o którym nikt inny nie wspomniał (zmienne typu o zasięgu) i zilustrował wszystkie pojęcia kodem i sesją GHCi. Gdyby możliwe było wybranie obu najlepiej, zrobiłbym to. Niestety nie mogę i po dokładnym przyjrzeniu się obu odpowiedziom zdecydowałem, że yairchu nieznacznie przewyższa Normana z powodu ilustracyjnego kodu i dołączonego wyjaśnienia. Jest to jednak trochę niesprawiedliwe, ponieważ naprawdę potrzebowałem obu odpowiedzi, aby zrozumieć to do tego stopnia, że forallnie odczuwam lekkiego strachu, gdy widzę to w podpisie typu.

Zacznijmy od przykładu kodu:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

Ten kod nie kompiluje się (błąd składniowy) w zwykłym Haskell 98. Wymaga rozszerzenia do obsługi forallsłowa kluczowego.

Zasadniczo istnieją 3 różne typowe zastosowania dla forallsłowa kluczowego (lub przynajmniej tak wydaje ), a każda z nich ma swoje własne rozszerzenia Haskell: ScopedTypeVariables, RankNTypes/ Rank2Types, ExistentialQuantification.

W powyższym kodzie nie pojawia się błąd składniowy przy żadnej z tych opcji, ale sprawdzane są tylko przy ScopedTypeVariableswłączonej.

Zmienne typu o zasięgu:

Zmienne typu o zasięgu pomagają określić typy kodu wewnątrz whereklauzul. To sprawia, że bw val :: btym samym co bw foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.

Zagmatwany punkt : możesz usłyszeć, że gdy pominiesz foralltyp, jest on nadal niejawnie obecny. ( z odpowiedzi Normana: „zwykle te języki pomijają forall z typów polimorficznych” ). To twierdzenie jest prawidłowe, ale odnosi się do innych zastosowań forall, a nie do ScopedTypeVariableswykorzystania.

Rodzaje rangi N:

Zacznijmy od tego, że mayb :: b -> (a -> b) -> Maybe a -> bjest to równoważne mayb :: forall a b. b -> (a -> b) -> Maybe a -> b, z wyjątkiem sytuacji, gdy ScopedTypeVariablesjest włączony.

Oznacza to, że działa dla każdego ai b.

Powiedzmy, że chcesz zrobić coś takiego.

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

Jaki musi być tego rodzaj liftTup? Jest liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b). Aby zobaczyć dlaczego, spróbujmy to zakodować:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

„Hmm… dlaczego GHC wnioskuje, że krotka musi zawierać dwa tego samego typu? Powiedzmy, że nie muszą”

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

Hmm więc tutaj GHC nie pozwala nam zastosować liftFuncna vbo v :: bi liftFuncchce x. Naprawdę chcemy, aby nasza funkcja otrzymała funkcję, która akceptuje każdą możliwą x!

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

Więc to nie liftTupdziała dla wszystkich x, to funkcja, którą dostaje, która działa.

Istnienie ilościowe:

Użyjmy przykładu:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

Czym różni się to od typów Rank-N?

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

Dzięki typom rang N forall aoznaczało, że twoje wyrażenie musi pasować do wszystkich możliwych as. Na przykład:

ghci> length ([] :: forall a. [a])
0

Pusta lista działa jak lista dowolnego typu.

Tak więc w przypadku Existential-Quantification, foralls w datadefinicjach oznacza, że ​​zawarta wartość może być dowolnego odpowiedniego typu, a nie że musi być wszystkich odpowiednich typów.

Czy ktoś może całkowicie wyjaśnić słowo kluczowe forall jasnym, prostym językiem angielskim?

Nie. (Może Don Stewart może.)

Oto bariery dla prostego, jasnego wyjaśnienia lub forall:

• To kwantyfikator. Musisz mieć przynajmniej trochę logiki (rachunek predykatów), aby zobaczyć uniwersalny lub egzystencjalny kwantyfikator. Jeśli nigdy nie widziałeś rachunku predykatu lub nie znasz się na kwantyfikatorach (a widziałem studentów, którzy nie czują się komfortowo podczas egzaminów kwalifikacyjnych), to nie ma dla ciebie łatwego wyjaśnienia forall.

• To kwantyfikator typu . Jeśli nie widziałeś Systemu F i ćwiczyłeś pisanie typów polimorficznych, będziesz forallmylić. Doświadczenie z Haskellem lub ML nie jest wystarczające, ponieważ zwykle te języki pomijają foralltypy polimorficzne. (Moim zdaniem jest to błąd w projektowaniu języka).

• W szczególności w Haskell foralljest używany w sposób, który wydaje mi się mylący. (Nie jestem teoretykiem typów, ale moja praca styka się z wieloma teoriami typów i całkiem nieźle się z tym czuję). Dla mnie głównym źródłem nieporozumień jest forallkodowanie typu, który Sam wolałbym pisać exists. Jest to uzasadnione trudnym izomorfizmem typu, obejmującym kwantyfikatory i strzałki, i za każdym razem, gdy chcę to zrozumieć, muszę to sprawdzić i sam opracować izomorfizm.

  Jeśli nie podoba ci się pomysł na izomorfizm typu, lub jeśli nie masz praktyki w myśleniu o izomorfizmie typu, to użycie go forallbędzie ci przeszkadzać.

• Podczas gdy ogólna koncepcja foralljest zawsze taka sama (zobowiązanie do wprowadzenia zmiennej typu), szczegóły różnych zastosowań mogą się znacznie różnić. Nieformalny angielski nie jest bardzo dobrym narzędziem do wyjaśniania różnic. Aby naprawdę zrozumieć, co się dzieje, potrzebujesz trochę matematyki. W tym przypadku odpowiednią matematykę można znaleźć we wprowadzającym tekście Benjamina Pierce'a Typy i języki programowania , który jest bardzo dobrą książką.

Jeśli chodzi o twoje konkretne przykłady,

• runST powinien sprawić, że głowa cię boli. Typy wyższego rzędu (wszystkie po lewej stronie strzałki) rzadko występują na wolności. Zachęcam do przeczytania artykułu, który przedstawił runST: „Leniwe wątki stanu funkcjonalnego” . To naprawdę dobry papier, który zapewni znacznie lepszą intuicję dla określonego typu runSTi ogólnie dla wyższych rang. Wyjaśnienie zajmuje kilka stron, jest bardzo dobrze zrobione i nie zamierzam tutaj go zagęszczać.

• Rozważać

  foo :: (forall a. a -> a) -> (Char,Bool)
  bar :: forall a. ((a -> a) -> (Char, Bool))

  Jeśli zadzwonię bar, mogę po prostu wybrać dowolny typ, aktóry mi się podoba, i mogę przekazać mu funkcję od typu ado typu a. Na przykład mogę przekazać funkcję (+1)lub funkcję reverse. Możesz pomyśleć o tym, forallże mówi „Teraz mogę wybrać typ”. (Słowo techniczne określające typ jest tworzone .)

  Ograniczenia wywoływania foosą znacznie bardziej rygorystyczne: argumentem foo musi być funkcja polimorficzna. W przypadku tego typu jedynymi funkcjami, które mogę przekazać, foosą idfunkcje, które zawsze się różnią lub popełniają błędy undefined. Powodem jest to, że z fooThe forallznajduje się na lewo od strzałki, tak jak wywołujący fooI nie dostać się do piłki, co aoznacza raczej, że to realizacja stanowi foo, że dostaje się wybrać to, co ajest. Ponieważ forallznajduje się po lewej stronie strzałki, a nie nad strzałką, jak w bar, instancja ma miejsce w treści funkcji, a nie w miejscu wywołania.

Podsumowanie: kompletne wyjaśnienie forallkluczowych wymaga matematyki i może być rozumiane tylko przez kogoś, kto studiował matematykę. Nawet częściowe wyjaśnienia są trudne do zrozumienia bez matematyki. Ale może moje częściowe, nie matematyczne wyjaśnienia trochę pomogą. Czytaj dalej Launchbury i Peyton Jones dalej runST!

Dodatek: żargon „powyżej”, „poniżej”, „po lewej stronie”. Nie mają one nic wspólnego z tekstowym sposobem pisania typów i wszystkim, co dotyczy drzew o składni abstrakcyjnej. W składni abstrakcyjnej a forallprzyjmuje nazwę zmiennej typu, a następnie występuje pełny typ „poniżej” forall. Strzałka przyjmuje dwa typy (typ argumentu i wynik) i tworzy nowy typ (typ funkcji). Typ argumentu znajduje się „po lewej stronie” strzałki; jest to lewe dziecko strzałki w drzewie składni abstrakcyjnej.

Przykłady:

• W forall a . [a] -> [a]forall znajduje się nad strzałą; co jest po lewej stronie strzałki [a].

• W

  forall n f e x . (forall e x . n e x -> f -> Fact x f) 
                -> Block n e x -> f -> Fact x f

  typ w nawiasach nazywa się „forall na lewo od strzałki”. (Używam tego typu w optymalizatorze, nad którym pracuję).

Moja oryginalna odpowiedź:

Czy ktoś może całkowicie wyjaśnić słowo kluczowe forall w jasnym, prostym języku angielskim

Jak wskazuje Norman, bardzo trudno jest podać jasne, jasne angielskie wyjaśnienie terminu technicznego z teorii typów. Wszyscy jednak próbujemy.

Jest tak naprawdę tylko jedna rzecz do zapamiętania o „forall”: wiąże typy z pewnym zakresem . Kiedy to zrozumiesz, wszystko jest dość łatwe. Jest to odpowiednik „lambda” (lub forma „let”) na poziomie czcionki - Norman Ramsey używa pojęcia „lewo” / „powyżej”, aby przekazać tę samą koncepcję zakresu w swojej doskonałej odpowiedzi .

Większość zastosowań „forall” jest bardzo prosta i można je znaleźć w Podręczniku użytkownika GHC, S7.8 ., Szczególnie doskonałe S7.8.5 na zagnieżdżonych formach „forall”.

W Haskell zwykle pomijamy spoiwo dla typów, gdy typ jest powszechnie kwanitowany, tak jak:

length :: forall a. [a] -> Int

jest równa:

length :: [a] -> Int

Otóż ​​to.

Ponieważ możesz teraz powiązać zmienne typu z pewnym zakresem, możesz mieć zakresy inne niż najwyższy poziom („ uniwersalnie kwantyfikowany ”), podobnie jak twój pierwszy przykład, w którym zmienna typu jest widoczna tylko w strukturze danych. Pozwala to na ukryte typy („ typy egzystencjalne ”). Lub możemy mieć dowolne zagnieżdżanie wiązań („typy rangi N”).

Aby głęboko zrozumieć systemy typów, musisz nauczyć się żargonu. Taka jest natura informatyki. Jednak proste zastosowania, takie jak powyżej, powinny być możliwe do zrozumienia intuicyjnie, poprzez analogię z „let” na poziomie wartości. Świetnym wprowadzeniem jest Launchbury i Peyton Jones .

Są gęsto wypełnione założeniami, że czytałem najnowsze w jakiejkolwiek gałęzi dyskretnej matematyki, teorii kategorii lub algebry abstrakcyjnej, która jest popularna w tym tygodniu. (Jeśli nigdy więcej nie przeczytam słowa „skonsultuj się z gazetą, aby poznać szczegóły realizacji”, będzie za wcześnie).

Eee, a co z prostą logiką pierwszego rzędu? forallcałkiem wyraźnie odnosi się do uniwersalnej kwantyfikacji iw tym kontekście termin egzystencjalny ma również większy sens, chociaż byłoby mniej niezręczne, gdyby istniało existssłowo kluczowe. To, czy kwantyfikacja jest rzeczywiście uniwersalna czy egzystencjalna, zależy od umiejscowienia kwantyfikatora w zależności od tego, gdzie zmienne są używane po której stronie strzałki funkcji, a wszystko to jest nieco mylące.

Tak więc, jeśli to nie pomoże, lub jeśli po prostu nie lubią logiki symbolicznej, z bardziej funkcjonalnych programowania-owski perspektywie można myśleć zmiennych typu jako po prostu (implicite) typu parametry do funkcji. Funkcje przyjmujące parametry typu w tym sensie są tradycyjnie pisane za pomocą dużej lambda z dowolnego powodu, który napiszę tutaj jako /\.

Rozważmy więc idfunkcję:

id :: forall a. a -> a
id x = x

Możemy przepisać go jako lambdas, przenosząc „parametr typu” poza podpis typu i dodając wbudowane adnotacje typu:

id = /\a -> (\x -> x) :: a -> a

To samo zrobiono, aby const:

const = /\a b -> (\x y -> x) :: a -> b -> a

Więc twój bar funkcja może wyglądać mniej więcej tak:

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

Zauważ, że typ funkcji został podany bar jako argument zależy od barparametru type. Zastanów się, czy zamiast tego masz coś takiego:

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

Oto bar2zastosowanie funkcji do czegoś typuChar , więc podanie bar2dowolnego parametru typu innego niżChar spowoduje błąd typu.

Z drugiej strony, oto co foo może wyglądać:

foo = (\f -> (f Char 't', f Bool True))

W przeciwieństwie do tego bar, foowcale nie przyjmuje żadnych parametrów typu! Pełni tę samą funkcję przyjmuje parametr typu, a następnie stosuje tę funkcję do dwóch różnych typów.

Więc kiedy widzisz forallw podpisie typu, pomyśl o tym jak o wyrażeniu lambda dla podpisów typu . Podobnie jak zwykłe lambdy, zakresforall rozszerzeń jest możliwie najdalej w prawo, aż do nawiasów okrągłych, i podobnie jak zmienne powiązane w zwykłej lambdzie, zmienne typu powiązane przezforall znajdują się w zakresie wyrażenia kwantyfikowanego.

Post Scriptum : Być może możesz się zastanawiać - skoro myślimy o funkcjach przyjmujących parametry typu, dlaczego nie możemy zrobić z tymi parametrami czegoś bardziej interesującego niż umieścić je w podpisie typu? Odpowiedź jest taka, że ​​możemy!

Funkcja, która łączy zmienne typu z etykietą i zwraca nowy typ, jest konstruktorem typów , który można napisać w ten sposób:

Either = /\a b -> ...

Potrzebowalibyśmy jednak zupełnie nowej notacji, ponieważ sposób zapisu takiego typu jest podobny Either a b sugeruje już „zastosowanie funkcjiEither do tych parametrów”.

Z drugiej strony funkcja, która niejako „dopasowuje wzorzec” parametrów parametrów typu, zwracając różne wartości dla różnych typów, jest metodą klasy typów . Nieznaczne rozszerzenie /\powyższej składni sugeruje coś takiego:

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

Osobiście uważam, że wolę właściwą składnię Haskella ...

Funkcja, która „dopasowuje” parametry swojego typu i zwraca dowolny, istniejący typ jest rodziną typów lub zależnością funkcjonalną - w poprzednim przypadku nawet już wygląda bardzo podobnie do definicji funkcji.

Oto krótkie i nieprzyzwoite wyjaśnienie w prostych słowach, które prawdopodobnie już znasz.

The forall kluczowe jest używane w Haskell tylko w jeden sposób. To zawsze oznacza to samo, kiedy go widzisz.

Uniwersalna kwantyfikacja

Powszechnie ilościowo typ to typ formy forall a. f a. Wartość tego typu można traktować jako funkcję, która przyjmuje typ a jako argument i zwraca wartość typu f a. Tyle że w Haskell argumenty tego typu są przekazywane niejawnie przez system typów. Ta „funkcja” musi dać ci tę samą wartość bez względu na to, jaki typ otrzyma, więc wartość jest polimorficzna .

Rozważmy na przykład typ forall a. [a]. Wartość tego typu pobiera inny typ ai zwraca listę elementów tego samego typu a. Oczywiście istnieje tylko jedna możliwa implementacja. Musi dać ci pustą listę, ponieważ amoże być absolutnie dowolnego typu. Pusta lista jest jedyną wartością listy, która jest polimorficzna w swoim typie elementu (ponieważ nie ma żadnych elementów).

Lub typ forall a. a -> a. Program wywołujący taką funkcję podaje zarówno typ, jak ai wartość typu a. Implementacja musi następnie zwrócić wartość tego samego typu a. Jest tylko jedna możliwa implementacja. Musiałby zwrócić taką samą wartość, jaką podano.

Egzystencjalna kwantyfikacja

Egzystencjalnie ilościowo rodzaj miałoby formę exists a. f a, jeśli Haskell poparła ten zapis. Wartość tego typu można traktować jako parę (lub „produkt”) składającą się z typu ai wartości typu f a.

Na przykład, jeśli masz wartość typu exists a. [a], masz listę elementów jakiegoś typu. Może to być dowolny typ, ale nawet jeśli nie wiesz, co to takiego, możesz wiele zrobić z taką listą. Możesz to odwrócić lub policzyć liczbę elementów lub wykonać dowolną inną operację na liście, która nie zależy od typu elementów.

OK, poczekaj chwilę. Dlaczego Haskell używa forallokreślenia „egzystencjalnego” takiego jak poniżej?

data ShowBox = forall s. Show s => SB s

Może to być mylące, ale tak naprawdę opisuje typ konstruktora danych SB :

SB :: forall s. Show s => s -> ShowBox

Po zbudowaniu możesz myśleć o wartości typu ShowBoxskładającej się z dwóch rzeczy. Jest to typ swraz z wartością typu s. Innymi słowy, jest to wartość egzystencjalnie skwantyfikowanego typu. ShowBoxmożna by naprawdę napisać tak exists s. Show s => s, jakby Haskell poparł ten zapis.

runST i przyjaciele

Biorąc to pod uwagę, czym się różnią?

foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Weźmy najpierw bar. Pobiera typ ai funkcję typu a -> ai tworzy wartość typu (Char, Bool). Możemy wybrać Intjako ai nadać mu Int -> Intna przykład funkcję typu . Ale foojest inaczej. Wymaga to, aby implementacja foobyła w stanie przekazać dowolny typ, jaki chce, do funkcji, którą mu nadamy. Zatem jedyną funkcją, którą moglibyśmy rozsądnie nadać, jest id.

Powinniśmy teraz być w stanie zająć się znaczeniem rodzaju runST:

runST :: forall a. (forall s. ST s a) -> a

runSTMusi więc być w stanie wygenerować wartość typu a, bez względu na to, jaki typ podamy a. Aby to zrobić, wykorzystuje argument typu, forall s. ST s aktóry z pewnością musi jakoś wygenerować a. Co więcej, musi być w stanie wygenerować wartość typu abez względu na typ, który implementacja runSTdecyduje się podać jakos .

Ok, i co? Zaletą jest to, że nakłada to ograniczenie na osobę dzwoniącą runST, ponieważ typ anie może w ogóle obejmować typu s. Nie możesz ST s [s]na przykład przekazać wartości typu . W praktyce oznacza to, że implementacja umożliwia runSTdowolną mutację o wartości typu s. Typ gwarantuje, że ta mutacja jest lokalna do wdrożenia runST.

Typ runSTjest przykładem typu polimorficznego rangi 2, ponieważ typ jego argumentu zawiera forallkwantyfikator. Typ foopowyższy ma również rangę 2. Zwykły typ polimorficzny, taki jak tego bar, ma rangę 1, ale staje się rangą 2, jeśli typy argumentów muszą być polimorficzne, z własnym forallkwantyfikatorem. A jeśli funkcja przyjmuje argumenty rangi 2, to jej typ to ranga 3 i tak dalej. Ogólnie rzecz biorąc, typ, który przyjmuje polimorficzne argumenty rangi, nma rangę n + 1.

Czy ktoś może całkowicie wyjaśnić słowo kluczowe forall jasnym, prostym językiem angielskim (lub, jeśli istnieje, wskazać tak jasne wyjaśnienie, którego mi brakowało), które nie zakłada, że ​​jestem matematykiem pogrążonym w żargonie?

Spróbuję wyjaśnić znaczenie i być może zastosowanie forall w kontekście Haskell i jego systemów typów.

Zanim jednak zrozumiecie, że chciałbym skierować was do bardzo przystępnej i miłej rozmowy Runara Bjarnasona zatytułowanej „ Ograniczenia wyzwolenia, ograniczenia wolności ”. Dyskusja jest pełna przykładów z rzeczywistych przypadków użycia, a także przykładów w Scali na poparcie tego stwierdzenia, chociaż nie wspomina o tym forall. Spróbuję wyjaśnić forallperspektywę poniżej.

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

Bardzo ważne jest, aby przeczytać i uwierzyć w to oświadczenie, aby kontynuować następujące wyjaśnienie, więc zachęcam do obejrzenia rozmowy (przynajmniej jej części).

Obecnie bardzo powszechnym przykładem pokazującym ekspresję systemu typów Haskell jest podpis tego typu:

foo :: a -> a

Mówi się, że biorąc pod uwagę ten typ podpisu, istnieje tylko jedna funkcja, która może spełnić ten typ i jest to identityfunkcja lub, co jest bardziej znane id.

Na początku nauki Haskell zawsze zastanawiałem się nad poniższymi funkcjami:

foo 5 = 6

foo True = False

oba spełniają powyższy podpis typu, dlaczego więc ludzie Haskell twierdzą, że idtylko on sam spełnia podpis typu?

Wynika to z faktu, że forallukryty podpis jest ukryty. Rzeczywisty typ to:

id :: forall a. a -> a

Wróćmy teraz do stwierdzenia: Ograniczenia wyzwalają, ograniczenia wolności

Po przetłumaczeniu tego na system typów ta instrukcja staje się:

Ograniczenie na poziomie typu staje się swobodą na poziomie terminu

i

Wolność na poziomie typu staje się ograniczeniem na poziomie terminu

Spróbujmy udowodnić pierwsze stwierdzenie:

Ograniczenie na poziomie typu.

Więc nakładając ograniczenie na nasz podpis typu

foo :: (Num a) => a -> a

staje się wolnością na poziomie terminów daje nam swobodę lub elastyczność w pisaniu tych wszystkich

foo 5 = 6
foo 4 = 2
foo 7 = 9
...

To samo można zaobserwować ograniczając a dowolną inną klasę typów itp

Więc teraz ten typ podpisu: foo :: (Num a) => a -> atłumaczy to:

∃a , st a -> a, ∀a ∈ Num

Jest to znane jako kwantyfikacja egzystencjalna, co oznacza, że istnieją pewne przypadki, adla których funkcja jest zasilana czymś typua zwraca coś tego samego typu, a wszystkie te instancje należą do zbioru liczb.

Dlatego widzimy, że dodanie ograniczenia (które apowinno należeć do zestawu liczb), uwalnia poziom terminu, aby mieć wiele możliwych implementacji.

Teraz dochodzę do drugiego stwierdzenia, które faktycznie zawiera wyjaśnienie forall:

Wolność na poziomie typu staje się ograniczeniem na poziomie terminu

Wyzwólmy teraz funkcję na poziomie typu:

foo :: forall a. a -> a

To przekłada się na:

∀a , a -> a

co oznacza, że ​​implementacja tego typu podpisu powinna być taka, a -> aaby dotyczyła wszystkich okoliczności.

Więc teraz zaczyna nas to ograniczać na poziomie terminu. Nie możemy już pisać

foo 5 = 7

ponieważ ta implementacja nie byłaby satysfakcjonująca, gdybyśmy umieścili ją ajako Bool. amoże być a Charlub a [Char]lub niestandardowym typem danych. We wszystkich okolicznościach powinien zwrócić coś podobnego typu. Ta swoboda na poziomie typu jest znana jako Universal Quantification, a jedyną funkcją, która może to zaspokoić

foo a = a

który jest powszechnie znany jako identityfunkcja

Stąd foralljest libertyna poziomie typu, którego rzeczywistym celem jest constrainokreślenie poziomu do konkretnej implementacji.

Powodem tego, że to słowo kluczowe jest różne, jest to, że jest ono używane w co najmniej dwóch różnych rozszerzeniach systemu typów: typy wyższego rzędu i egzystencjalne.

Prawdopodobnie najlepiej jest po prostu przeczytać i zrozumieć te dwie rzeczy osobno, zamiast próbować wyjaśnić, dlaczego „forall” jest odpowiednią częścią składni jednocześnie.

Jak egzystencjalny egzystencjalny?

W przypadku oceny egzystencjalnej foralls w datadefinicjach oznacza, że ​​zawarta wartość może być dowolnego odpowiedniego typu, a nie, że musi być wszystkich odpowiednich typów. - odpowiedź yachiru

Wyjaśnienie, dlaczego forallw datadefinicjach są izomorficzne (exists a. a)(pseudo-Haskell), można znaleźć w „Haskell / typy ilościowo określone” w Wikibooks .

Oto krótkie, pełne podsumowanie:

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

MkT xJaki jest typ dopasowywania / dekonstrukcji wzorów x?

foo (MkT x) = ... -- -- what is the type of x?

xmoże być dowolnego typu (jak podano w forall), więc jego typ to:

x :: exists a. a -- (pseudo-Haskell)

Dlatego następujące są izomorficzne:

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

forall oznacza forall

Moją prostą interpretacją tego wszystkiego jest to, że „ forallnaprawdę oznacza„ dla wszystkich ””. Ważnym rozróżnieniem jest wpływ forallna definicję a zastosowanie funkcji .

A foralloznacza definicję wartości lub funkcji musi być polimorficzna.

Jeśli definiowana rzecz jest wartością polimorficzną , oznacza to, że wartość musi być poprawna dla wszystkich odpowiednich a, co jest dość restrykcyjne.

Jeśli definiowana rzecz jest funkcją polimorficzną , oznacza to, że funkcja musi być poprawna dla wszystkich odpowiednich a, co nie jest aż tak restrykcyjne, ponieważ tylko dlatego, że funkcja jest polimorficzna, nie oznacza, że zastosowany parametr musi być polimorficzny. Oznacza to, że jeśli funkcja jest ważna dla wszystkich a, to odwrotnie każdy odpowiedni amoże być zastosowany do funkcji. Jednak typ parametru można wybrać tylko raz w definicji funkcji.

Jeśli a foralljest w typie parametru funkcji (tj. A Rank2Type), oznacza to, że zastosowany parametr musi być naprawdę polimorficzny, aby być zgodny z ideą definicjiforall środka jest polimorficzny. W takim przypadku typ parametru można wybrać więcej niż jeden raz w definicji funkcji ( „i jest wybierany przez implementację funkcji”, jak wskazał Norman )

Dlatego powód egzystencjalne datadefinicje umożliwia dowolny a dlatego konstruktor danych jest polimorficzny funkcja :

MkT :: forall a. a -> T

rodzaj MkT :: a -> *

Co oznacza, aże do funkcji można zastosować dowolny . W przeciwieństwie do, powiedzmy, wartości polimorficznej :

valueT :: forall a. [a]

rodzaj wartości T :: a

Co oznacza, że definicja valueT musi być polimorficzna. W takim przypadku valueTmożna zdefiniować jako pustą listę []wszystkich typów.

[] :: [t]

Różnice

Chociaż znaczenie dla foralljest spójne w ExistentialQuantificationi RankNType, egzystencjalność ma tę różnicę, że datakonstruktor może być używany w dopasowywaniu wzorców. Jak udokumentowano w instrukcji obsługi ghc :

Podczas dopasowywania wzorca każde dopasowanie wzorca wprowadza nowy, odrębny typ dla każdej zmiennej typu egzystencjalnego. Te typy nie mogą być zunifikowane z żadnym innym typem, ani nie mogą uciekać z zakresu dopasowania wzorca.