2016-11-23 13 views
8

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?

+0

Nie sądzę, że to powinno zadziałać. Jednak jest to całkowicie nieszkodliwe, ponieważ synonimy są rozszerzone w sprawdzaniu typów. – dfeuer

+1

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

+1

@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

Odpowiedz

2

Odpowiadam na moje własne pytanie z informacjami pobranymi z komentarzy dfeuer i user2407038.

Okazało się, że mój kod zrobił naruszać wymaganie nasycenia. Nie znalazłem błędu z powodu dziwnego zachowania (błędu?) Z :kind! w ghci. Ale wpisanie tego samego typu w pliku hs powoduje błąd kompilacji.

TyCon1 nie jest przeznaczony dla rodzin typów, ale do zawijania zwykłych konstruktorów typów, takich jak Maybe, które nie mają problemu z ujednoliceniem ze zmiennymi typu. type Foo = Map (TyCon1 Maybe) '[Char,Int] działa dobrze, na przykład.

Dla rodzin typów należy zdefiniować specjalny typ pomocniczy dla każdego z nich, a następnie zdefiniować instancję Apply dla typu. Tak:

data FlipSym :: TyFun * * -> * 
type instance Apply FlipSym x = Flip x 

type Boo = Map FlipSym '[Char,Int] 

Zauważ, że w ten sposób rodzina Flip typ nie jest ujednolicenie z dowolnej zmiennej typu.

+1

Przepraszam, że nie udało mi się samodzielnie udzielić odpowiedzi. Twoja jest co najmniej tak dobra jak to, co napisałbym. Jedna nitka, którą chciałbym wybrać: nie podoba mi się nazwa "Flip" dla tej rodziny. Moim zdaniem, nazwa ta jest zawsze zdefiniowana jako "newtype Flip (f :: j -> k -> *) (y :: k) (x :: j) = Flip {unFlip :: f x y}'.Wynikowa wersja 'flip' pojawia się dość często i ogólnie w kontekstach, w których wersja synonimów typu (' type Flip xy = f x y') nie byłaby przydatna. – dfeuer

Powiązane problemy