Przekształcanie GADT bez ograniczeń w inny GADT z ograniczeniami, gdy takie więzy zatrzymają się.

Question

Czy możemy przekształcić GADT bez danego ograniczenia na jego konstruktorach na GADT, który ma wspomniane ograniczenie? Chcę to zrobić, ponieważ chcę uzyskać głębokie osadzenie Arrows i zrobić kilka interesujących rzeczy z reprezentacją, która (na razie) wydaje się wymagać Typeable. (One reason)

data DSL a b where 
    Id :: DSL a a 
    Comp :: DSL b c -> DSL a b -> DSL a c 
    -- Other constructors for Arrow(Loop,Apply,etc) 

data DSL2 a b where 
    Id2 :: (Typeable a, Typeable b)    => DSL2 a a 
    Comp2 :: (Typeable a, Typeable b, Typeable c) => DSL2 b c -> DSL2 a b -> DSL2 a c 
    -- ... 

Mogliśmy wypróbować następującą from funkcję ale łamie szybko jak my nie mają Typeable informacje dla punktu rekurencyjnego

from :: (Typeable a, Typeable b) => DSL a b -> DSL2 a b 
from (Id)  = Id2 
from (Comp g f) = Comp2 (from g) (from f) 

Zamiast więc staramy się uchwycić transformacji w klasie typu. Jednak to się załamie, a my będziemy tracić informacje, ponieważ b jest egzystencjalnym.

class From a b where 
    from :: a -> b 

instance (Typeable a, Typeable b) => From (DSL a b) (DSL2 a b) where 
    from (Id)  = Id2 
    from (Comp g f) = Comp2 (from g) (from f) 

Jakieś inne sugestie? Ostatecznie chcę utworzyć głębokie osadzanie Category i Arrow wraz z Typeable informacji o parametrach typu. Jest tak, że mogę użyć składni strzałki, aby skonstruować wartość w moim DSL i mieć dość standardowy kod Haskella. Może muszę uciekać się do szablonu Haskella?

Answer 1

Problem z rekurencyjnym przypadkiem jest śmiertelny w przekształcaniu DSL a b w DSL2 a b.

Aby to zrobić transformacja wymagałoby znalezienia słownika Typeable dla egzystencjalnej typu b w przypadku Comp - ale co b rzeczywiście jest już zapomniane.

Na przykład rozważmy następujący program:

data X = X Int 
-- No Typeable instance for X 

dsl1 :: DSL X Char 
dsl1 = -- DSL needs to have some way to make non-identity terms, 
     -- use whatever mechanism it offers for this. 

dsl2 :: DSL Int X 
dsl2 = -- DSL needs to have some way to make non-identity terms, 
     -- use whatever mechanism it offers for this. 

v :: DSL Int Char 
v = Comp dsl1 dsl2 

v2 :: DSL2 Int Char 
v2 = -- made by converting v from DSL to DSL2, note that Int and Char are Typeable 

typeOfIntermediate :: DSL a c -> TypeRep 
typeOfIntermediate int = 
    case int of 
     Comp (bc :: DSL2 b c) (ab :: DSL2 a b) -> 
      typeOf (undefined :: b) 

typeOfX = typeOfIntermediate v2 

Innymi słowy, jeśli istnieje sposób, aby zrobić konwersję w ogóle, można jakoś wynaleźć instancji Typeable dla typu, który w rzeczywistości nie mają jedną .

Answer 2

Docelowo chcę stworzyć głęboko osadzanie Category i Arrow wraz z Typeable informacji na temat parametrów typu. Jest tak, że mogę użyć składni strzałki, aby skonstruować wartość w moim DSL i mieć dość standardowy kod Haskella.

Może trzeba uciekać się do {-# LANGUAGE RebindableSyntax #-} (odnotowując, że implikuje NoImplicitPrelude). Stwórz własne funkcje, a GHC użyje ich podczas usuwania strzałki, zamiast standardowych wersji z Control.Arrow.

Instrukcja podaje, że "typy tych funkcji muszą być bardzo podobne do typów Prelude". Jeśli budujesz równoległą hierarchię klas (kopię hierarchii w Control.Arrow, ale z ograniczeniami Typeable dodanymi do sygnatur typu), powinieneś być w porządku.

(n.b. Nie znam notacji strzałek, więc nigdy nie użyłem jej w połączeniu z RebindableSyntax, moja odpowiedź brzmi inteligentnie.)