Pomoc w programowaniu, odpowiedzi na pytania / Haskell / Haskell Weird Kinds: Rodzaj (->) jest ?? ->? -> * - haskell, typy, systemy typów

Haskell Weird Kinds: Kind of (->) is? ->? -> * - haskell, typy, systemy typu

Kiedy eksperymentowałem z rodzajami Haskella i starałem się uzyskać tego rodzaju ->, a to pokazało:

$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude>

Zamiast oczekiwanego * -> * -> *. Jakie są ?? i ? rzeczy? Czy mają na myśli konkretne typy czy „miłe zmienne”? Albo coś innego?

Odpowiedzi:

96 dla odpowiedzi nr 1

Są to specyficzne dla GHC rozszerzenia systemu rodzaju Haskell. Raport Haskell 98 określa tylko prosty rodzaj systemu:

... wyrażenia typu są klasyfikowane na różne rodzaje, które biorą jeden dwóch możliwych form:

Symbol * reprezentuje rodzaj wszystkie konstruktory typu zerowego. Jeśli k1 i k2 są rodzajami, wtedy k1-> k2 jest rodzaj rodzajów, które mają rodzaj k1 i zwraca rodzaj rodzaju k2.

GHC rozszerza ten system z pewnego rodzaju podtypami, aby pozwolić typy rozpakowane, i aby pozwolić konstruktorowi funkcji na polimorficzny w stosunku do rodzajów. Rodzaj sieci obsługiwanej przez GHC to:

             ?
/
/  
??   (#)
/ 
*   #

Where:       *   [LiftedTypeKind]   means boxed type
#   [UnliftedTypeKind] means unboxed type
(#)  [UbxTupleKind]     means unboxed tuple
??   [ArgTypeKind]      is the lub of {*, #}
?    [OpenTypeKind]     means any type at all

Zdefiniowany w ghc / compiler / types / Type.lhs

W szczególności:

> error :: forall a:?. String -> a
> (->)  :: ?? -> ? -> *
> (\(x::t) -> ...)

Gdzie w ostatnim przykładzie t :: ?? (tj. nie jest krotką bez opakowania). Tak więc, cytując GHC, „na poziomie rodzaju istnieje niewielkie poddziałanie”.

W przypadku zainteresowanych dusz GHC obsługuje również typy i rodzaje przymusu („warunki na poziomie rodzaju, które działają jako dowód na równość typów”, zgodnie z potrzebami System Fc) stosowane w GADT, nowych typach i rodzinach typów.