Haskell GADTs конструктор

Question

У меня есть следующие

data Expr = Condition v 
      | And Expr Expr 
      | Or Expr Expr 

и я попросил рассмотреть следовать нетипизированной версию для завершения:

data Expr e where 

Я не уверен, что я полагаю, напишите для конструкторов. Я попытался следующие:

data Expr e where 
    Condition :: v -> Expr v 
    And :: -- really not sure what to do with this one 
    OR :: Expr b -> (Expr b -> Expr a) -> Maybe Expr a -> Expr b 

Кроме того, поскольку v может быть любого типа, т.е. int, bool и т.д. возможно только назвать следующие (вверху) и объявить тип v позже?

data v = IntVat int 

любая помощь была бы оценена :)

EDIT: изменил весь пост, чтобы добавить немного больше информации и ясности (на основе моего понимания упражнения).

В основном мне нужна помощь в определении конструкторов для GADT с учетом data Expr = Condition v...etc в качестве ссылки.

Answer 1

Если бы я задавал назначение на GADT, используя основной язык выражения в качестве мотивационного примера, вот такой ответ я имею в виду:

data Expr v where 
    Literal :: v -> Expr v 
    And  :: Expr Bool -> Expr Bool -> Expr Bool 
    Or  :: Expr Bool -> Expr Bool -> Expr Bool 
    -- and I'd probably add some things like this to 
    -- show why the type variable is useful 
    Equal :: Expr Int -> Expr Int -> Expr Bool 
    If  :: Expr Bool -> Expr v -> Expr v -> Expr v 

вы можете понять, почему вы могли бы назвать это «напечатанный» выражение: в конкретизации переменных типа выглядят как вводить правила для небольшого языка:

a : Bool   b : Bool 
------------------------- 
    And a b : Bool 

a : Int   b : Int 
------------------------ 
    Equal a b : Bool 

и т.д.

Answer 2

Это звучит как экзистенциальный тип для меня. Должен признаться, я никогда их не использовал, я только пытался их понять; в любом случае, может быть, это означает, как это:

data Expr = forall v. Condition v 
      | And Expr Expr 
      | Or Expr Expr 

Тогда вы имели GADT подобное (они обобщают экзистенциалам см here):

data Expr where 
    Condition :: v -> Expr 
    And :: Expr -> Expr -> Expr 
    Or :: Expr -> Expr -> Expr 

Хотя, что бы не (насколько я понял концепция) имеют смысл, поскольку вы не можете использовать v для чего-либо.

С другой стороны, это бы (я надеюсь) больше смысла (так как есть «состояние»):

class Testable v where 
    test :: v -> Bool 

data Expr where 
    Condition :: Testable v => v -> Expr 
    And :: Expr -> Expr -> Expr 
    Or :: Expr -> Expr -> Expr 

, то вы могли бы сделать, например,

eval :: Expr -> Bool 
eval (Condition v) = test v 
eval (And e1 e2) = (eval e1) && (eval e2) 
eval (Or e1 e2) = (eval e1) || (eval e2) 

, который будет работать для различных видов «условий».

Я не тестировал этот код, и, как я уже сказал, я не профессионал в экзистенциальности. Я надеюсь, что мой код верен, но, пожалуйста, скажите мне кого-нибудь, если вы знаете лучше (или я полностью ошибаюсь ...)