Объяснение нетипизированных терминов

Question

У меня есть продолжение упражнения из универа для моего предмета Haskell, где я был дан следующий:

data Expr = Con Value 
      | And Expr Expr 

data Value = IntValue Int 
      | BoolValue Bool 

est :: Expr -> Val 
est (Con v) = v 
est (And x y) = 
    case (est x, est y) of 
    (BoolValue bool1, BoolValue bool2) -> BoolValue $ bool1 && bool2 
    _     -> error "And: expected Boolean arguments" 

И я не уверен, что это действительно делает. Он, по-видимому, является оценщиком терминов, определенных в Expr. Может ли кто-нибудь объяснить это мне? Мое упражнение включает меня преобразование, что в GADTs, который я сделал, как:

data Expr e where 
    Con :: Val -> Expr Val 
    And :: Expr e -> Expr e -> Expr e 

Теперь они просят меня осуществить следующим статический и сделать его типобезопасно:

est :: Expr e -> e 
est _ = -- implement this 

Answer 1

Я думаю, что вы ошиблись на своем GADT. Чтобы понять, почему мы сначала рассмотрим нетипизированную версию Expr и ее оценщика (первая часть вашего вопроса).

Вот несколько значений типа Expr которые можно построить:

expr1 = Con (IntValue 42) 
expr2 = Con (BoolValue True) 
expr3 = Con (BoolValue False) 

До сих пор так хорошо: expr1 представляет собой целое число, постоянная 42, expr2 и expr3 булевы константы True и False. Все значения типа Expr с Con, как их внешний конструктор, по существу выглядят так.

Вещи начинают получать интересно, когда мы добавим And конструктор смеси:

expr4 = And (Con (BoolValue True)) (Con (BoolValue True)) 
expr5 = And (Con (BoolValue True)) (And (Con (BoolValue False)) (Con (BoolValue False))) 
expr6 = And (Con (BoolValue True)) (Con (IntValue 42)) 

expr4 и expr5 прекрасны; они представляют собой выражения True && True и True && (False && False), соответственно. Мы ожидаем, что они оценят до True и False, но об этом скоро. Однако expr6 выглядит подозрительно: он представляет выражение True && 42, которое не имеет смысла (по крайней мере, в Haskell!).

выражения мы видели до сих пор, за исключением числа 6, все они имеют значение: expr1 имеет целочисленное значение 42, остальные булевы (True, False, True, False для expr с 2 по 5). Как вы можете видеть, значения являются целыми или логическими и поэтому могут быть представлены как значения типа Value.

Мы можем написать эксперт, который принимает Expr и возвращает его Value. В словах оценщик должен вернуть значение константного выражения, и если выражение является логическим «и», оно должно возвращать логические значения «и» значений составных выражений, которые должны быть, чтобы быть логическими значениями - вы можете 'возьмите логическое число and целого числа и булево или два целых числа. В коде, это приводит к

est :: Expr -> Value -- takes an Expr and returns its Value 
est (Con value) = value -- the value of a constant expression is the wrapped value 
est (And e1 e2) = let value1 = est e1 -- the value of the first operand 
         value2 = est e2 -- the value of the second operand 
        in logicalAndValue value1 value2 

logicalAndValue :: Value -> Value -> Value 
logicalAndValue (BoolValue b1) (BoolValue b2) = BoolValue (b1 && b2) 
logicalAndValue (BoolValue b1) (IntValue i2) = error "Can't take the logical 'and' of a boolean and an integer" 
logicalAndValue (IntValue i1) (BoolValue b2) = error "Can't take the logical 'and' of an integer and a boolean" 
logicalAndValue (IntValue i1) (IntValue i2) = error "Can't take the logical 'and' of two integers" 

Это просто более подробная версия первого est с операцией взятия логического «и» двух вычисленных выражений, выделившихся в отдельную функцию и немного более информативных ошибки Сообщения.

Хорошо, надеюсь, это отвечает на ваш первый вопрос! Проблема сводится к тому, что значения Expr могут иметь либо логическое, либо целочисленное значение, и вы больше не можете «видеть» этот тип, так что возможно And двух выражений, для которых это не имеет смысла.

---

Одним из способов решения этой проблемы было бы разделить на две Expr новых типов экспрессии, один из которых содержит целые значения, а другой с логическими значениями. Это будет выглядеть примерно так (я дам эквиваленты expr с используемыми выше, а):

data IntExpr = ConInt Int 
expr1 :: IntExpr 
expr1 = ConInt 42 

data BoolExpr = ConBool Bool 
       | AndBool BoolExpr BoolExpr 
expr2 :: BoolExpr 
expr2 = ConBool True 
expr3 = ConBool False 
expr4 = AndBool (ConBool True) (ConBool True) 
expr5 = AndBool (ConBool True) (AndBool (ConBool False) (ConBool False)) 

Две вещи интересно отметить: мы избавились от Value типа, и теперь он стал невозможно построить эквивалент expr6 - это потому, что его очевидный перевод AndBool (ConBool True) (ConInt 42) будет отклонен компилятором (возможно, стоит попробовать это) из-за ошибки типа: ConInt 42 имеет тип IntExpr, и вы не можете использовать это как второй аргумент AndBool.

Оценщику также понадобятся две версии: одна для целых выражений и одна для булевых выражений; давайте напишем их! IntExpr должны иметь Int значение, и BoolExpr следует оценивать в Bool с:

evalInt :: IntExpr -> Int 
evalInt (ConInt n) = n 

evalBool :: BoolExpr -> Bool 
evalBool (ConBool b) = b 
evalBool (AndBool e1 e2) = let v1 = evalBool e1 -- v1 is a Bool 
           v2 = evalBool e2 -- v2 as well 
          in v1 && v2 

Как вы можете себе представить, это будет получить утомительно быстро, как вы добавите больше типов выражений (как Char, списки, Double) или способов объединить такие выражения, как сложение двух чисел, построение «если» выражения или даже переменные, где тип не дано заранее ...

---

Это где GADTs заходи! Вместо того, чтобы делать отдельный тип выражения для каждого возможного типа результата оценки (IntExpr и BoolExpr выше), мы собираемся «пометить» тип выражения самим типом, который он будет оценивать.Таким образом, мы будем уверены, что результат вычисления значения типа Expr Int будет Int и что Expr Bool предоставит нам Bool. Фактически, мы дадим компилятору выполнить проверку типов для нас, вместо того, чтобы делать это во время выполнения (как в функции logicalAndValue выше).

На данный момент у нас есть только два способа построения выражений: создание постоянного выражения и «и» объединение двух булевых значений. Первый способ работает следующим образом: если у нас есть Int, мы превращаем его в Expr Int, Bool превращается в Expr Bool и так далее. Таким образом, типа подпись для конструктора «сделать постоянное выражение» будет:

Con :: v -> Expr v 

Второй конструктор принимает два выражения, которые представляют собой логические значения (так что эти два выражения типа Expr Bool) и возвращает другое выражение с булевым значение, то есть тип этого конструктора

And :: Expr Bool -> Expr Bool -> Expr Bool 

Ввод куски вместе, мы получаем следующее Expr типа:

data Expr e where 
    Con :: v -> Expr v 
    And :: Expr Bool -> Expr Bool -> Expr Bool 

Некоторые примеры значений:

expr1 :: Expr Int 
expr1 = Con 42 
expr2 :: Expr Bool 
expr2 = Con True 
expr3 :: Expr Bool 
expr3 = Con False 
expr4 :: Expr Bool 
expr4 = And (Con True) (Con True) 
expr5 :: Expr 
expr5 = And (Con True) (And (Con False) (Con False)) 

Еще раз, что эквивалентно expr6 не проходит проверки типов: было бы And (Con True) (Con 42), но Con 42 является Expr Int и, следовательно, не может быть использована в качестве аргумента And - он должен быть Expr Bool.

Оценщик становится действительно легко сейчас. Учитывая Expr e (помните, это означает, что это выражение, которое имеет значение типа e), оно возвращает e. Значение константного выражения - это сама константа, а значение логического выражения «и» - это «и» значений операндов, и мы уверены, что эти значения равны Bool. Это дает:

est :: Expr e -> e 
est (Con v) = v 
est (And e1 e2) = let b1 = est e1 -- this will be a Bool, since e1 is an Expr Bool 
         b2 = est e2 -- likewise 
        in b1 && b2 

---

GADT вы дали это прямой эквивалент бестипового Expr, и он будет по-прежнему позволяют строить «плохих» ценности, такие как And (Con (BoolValue True)) (Con (IntValue 42)).

Избавляясь от типа «Значение», мы можем быть более точными в том, что означает тип выражения; вместо того, чтобы говорить: «Тип выражения - целое или логическое, но я еще не знаю» и сталкиваясь с проблемами при оценке выражений, мы с самого начала убеждаемся в том, что мы знаем тип значения выражения и что мы не объединяем их таким образом, чтобы это не имело смысла.

Надеюсь, вы сделали это до сих пор - все эти типы, ценности и выражения на разных уровнях могут запутаться! - и вы сможете немного поэкспериментировать с расширением типа Expr и оценщика самостоятельно.

Простые вещи, которые нужно попробовать, составляют выражение, которое добавляет два целочисленных значения, используя константу string или char, или выражение 'if-then-else', которое принимает три аргумента: первый из булевых типов, второй и треть такого же типа (но этот тип может быть Int, Bool, Char или что-то еще).

Answer 2

точкой использование GADT должно гарантировать, что все выражения хорошо типизированы по строительству. Это означает, что если у вас есть Expr Int, вы знаете, что он хорошо типизирован и что он оценивает Int.

Для обеспечения этого, необходимо убедиться, что постоянные выражения с тегами типа они содержат, так что Con 0 имеет тип Expr Int в то время как Con True является Expr Bool.

Con :: v -> Expr v 

Кроме того, вы должны убедиться, что And могут быть использованы только в выражениях, которые оценивают в Bool.

And :: Expr Bool -> Expr Bool -> Expr Bool 

Таким образом, что-то вроде Con 0 `And` Con 1 даже не компилируется, так как константы имеют тип Expr Int в то время как And требует Expr Bool.

Как только вы правильно настроили это, выполнение est :: Expr e -> e должно быть тривиальным упражнением.