SpodziewamKind podpisy i typ rodziny
type family Rep a
i
type family Rep :: * -> *
być taka sama, ale wydaje się, że istnieje różnica
type family Rep a
type instance Rep Int = Char
-- ok
type family Rep :: * -> *
type instance Rep Int = Char
-- Expected kind * -> *, but got 'Int' instead
Czy ja po prostu potknął Błąd rozszerzenia Haskell, czy jest jakiś sens takiego zachowania?
Tak, istnieje subtelna różnica.
grubsza type family F a :: *->* stwierdza, że, powiedzmy, F Int jest injective typ konstruktor jak [], Maybe. Ten jest wykorzystywany przez kompilator, który można wpisać sprawdzić poniższy kod:
type family F a :: * -> *
-- these three examples can be removed/changed, if wished
type instance F Int = []
type instance F Char = Maybe
type instance F Bool = (,) String
foo :: (F Int a :~: F Int b) -> (a :~: b)
foo Refl = Refl
Aby wpisać sprawdzić powyżej, kompilator wykorzystał fakt, że F Int a ~ F Int b implikuje a ~ b, co wynika z zatłaczania gazu.
Zamiast tego deklarowanie type family F a b :: * nie zapewnia skuteczności iniekcji F Int, ponieważ poniższe zasady stają się dozwolone.
type family F a b :: *
type instance F Int a =()
Punkt jest typem rodziny nie są "funkcje poziomu poziomie". Są to "rodziny typów". Powinieneś zobaczyć syntaktyczne podobieństwa pomiędzy dopasowaniem wzorców na poziomie wartości i typami deklaracji instancji rodziny jako zbiegiem okoliczności - te dwie mają zupełnie inną semantykę (np. Spróbuj wpisać funkcję poziomu wartości, która pasuje do konstruktora 'Left :: a -> Any ab '). Jesteś już świadkiem minimalnego przykładu różnicy. Rodzina drugiego typu jest po prostu synonimem typu, ponieważ może mieć tylko jedną instancję. Pierwsza to właściwa rodzina typów. – user2407038
Chciałbym mieć prosty sposób wyjaśnienia różnicy między "funkcją na poziomie typu" i "rodziną typów", ale ja nie. Różnica sprowadza się do tego, że pierwsza rodzina typów nie może być częściowo zastosowana (ani druga, oczywiście, ale każde użycie drugiej to aplikacja nasycona, ponieważ przyjmuje 0 argumentów) - innymi słowy, 1. typ rodzina nie ma rodzaju, który można przypisać do niej w systemie typu Haskell. – user2407038