mam ten minimalny przykład roboczy (zaczerpnięte z biblioteki singletons) mapowania rodzinę typ na liście Typ szczebla:Dlaczego ten kod nie narusza "wymagań dotyczących nasycenia rodzin typów"?
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
data TyFun :: * -> * -> *
data TyCon1 :: (k1 -> k2) -> (TyFun k1 k2 -> *)
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
type instance Apply (TyCon1 f) x = f x
type family Map (f :: TyFun a b -> *) (as :: [a]) :: [b] where
Map f '[] = '[]
Map f (x ': xs) = Apply f x ': Map f xs
type family Flip t :: * where
Flip Int = Char
Flip Char = Int
wydaje się działać:
ghci> :set -XDataKinds
ghci> :kind! Map (TyCon1 Flip) '[Char,Int]
Map (TyCon1 Flip) '[Char,Int] :: [*]
= '[Int, Char]
Kod jest wyjaśnione w poście Defunctionalization for the win. Jest to obejście tego, że "GHC nie pozwoli zmiennej typu ujednolicić z rodziną typów". Nazywa się to "wymaganiem nasycenia rodzin typów".
Moje wątpliwości to: kiedy „run” :kind! Map (TyCon1 Flip) '[Char,Int]
wydaje się, że w linii type instance Apply (TyCon1 f) x = f x
, f
zostaną dopasowane naszej Flip
typu rodziny. Dlaczego to nie narusza wymogu nasycenia?
Nie sądzę, że to powinno zadziałać. Jednak jest to całkowicie nieszkodliwe, ponieważ synonimy są rozszerzone w sprawdzaniu typów. – dfeuer
Sądzę, że naprawdę należy dostarczyć symbol defunctionalization dla 'Flip' z własną instancją' Apply'. 'TyCon1' jest przeznaczony do stosowania do konstruktorów typów. A propos, jaka wersja GHC jest taka? – dfeuer
@dfeuer Używam GHC 8.0.1. Najwyraźniej rzecz działa przy użyciu ': kind!' W ghci, ale jeśli spróbuję dodać coś takiego jak 'type Boo = Map (TyCon1 Flip) '[Char, Int]' do skryptu, to spowoduje to błąd kompilacji. – danidiaz