Как создать функцию Haskell, которая будет вводить новый тип? - PullRequest
Новая
       22

Как создать функцию Haskell, которая будет вводить новый тип?

7 голосов
/ 10 декабря 2010

Я сейчас пишу парсер выражений.Я провел лексический и синтаксический анализ и теперь проверяю типы.У меня есть выражение в структуре данных, как это (упрощенная версия): 

data Expr = EBinaryOp String Expr Expr
          | EInt Int
          | EFloat Float

И теперь мне нужна функция, которая преобразует это в новый тип, скажем TypedExpr, который также будет содержать информацию о типе,И теперь моя главная проблема в том, как этот тип должен выглядеть.У меня есть две идеи - с параметром типа: 

data TypedExpr t = TEBinaryOp (TBinaryOp a b t) (TExpr a) (TExpr b)
                 | TEConstant t
addTypes :: (ExprType t) => Expr -> TypedExpr t

или без: 

data TypedExpr = TEBinaryOp Type BinaryOp TypedExpr TypedExpr
               | TEConstant Type Dynamic
addTypes :: Expr -> TypedExpr

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

Можно ли сделать это с помощью первого параметра?
Какой вариант вы бы выбрали?Почему?
Какие проблемы мне следует ожидать с каждым вариантом?

Ответы [ 3 ]

10 голосов
/ 10 декабря 2010

Тип вашей функции 

addTypes :: Expr -> TypedExpr t

неправильный, потому что это будет означать, что вы получите TypedExpr t для любого t, который вам нравится .Напротив, на самом деле вам нужен один конкретный t, который определяется аргументом типа Expr.

. Это рассуждение уже показывает, что вы выходите за пределы возможностейСистема типов Хиндли-Милнера.В конце концов, возвращаемый тип из addTypes должен зависеть от значения аргумента, но в простом Haskell 2010 типы могут не зависеть от значений.Следовательно, вам нужно расширение системы типов, которое приблизит вас к зависимым типам .В Haskell это могут сделать обобщенные алгебраические типы данных (GADT).

Для первого знакомства с GADT см. Также мое видео о GADT .

Однако, после ознакомления с GADT, у вас все еще остается проблема разбора нетипизированного выражения в типизированное, т.е. написать функцию 

addTypes :: Expr -> (exists t. TypedExpr t)

Конечно, вы должны выполнить некоторую проверку типа самостоятельноНо даже тогда непросто убедить компилятор Haskell, что ваши проверки типов (которые происходят на уровне значений) могут быть подняты до уровня типов.К счастью, другие люди уже подумали об этом, например, посмотрите следующее сообщение в списке рассылки haskell-cafe:

Эдвард Кметт .
Re: Ручной тип-Проверка предоставления экземпляров Read для GADT.(было Re: [Haskell-cafe] Читать экземпляр для GATD)
http://article.gmane.org/gmane.comp.lang.haskell.cafe/76466

(Кто-нибудь знает о официально опубликованной / хорошо написанной ссылке?)

4 голосов
/ 10 декабря 2010

Я недавно начал использовать финальный синтаксис без тегов для встроенных DSL, и я обнаружил, что он гораздо лучше стандартного метода GADT (к которому вы идете, и описывает Апфельмус).

Ключ к окончательному синтаксису тегов заключается в том, что вместо использования типа данных выражения вы представляете операции с классом типа. Для таких функций, как ваша eBinaryOp, я считаю, что лучше всего использовать два класса: 

class Repr repr where
  eInt :: repr Int
  eFloat :: repr Float

class Repr repr => BinaryOp repr a b c where
  eBinaryOp :: String -> repr a -> repr b -> repr c

Я бы сделал отдельные функции BinaryOp, а не использовал бы String. На веб-странице Олега есть намного больше информации, включая парсер, использующий систему типов Haskell.

3 голосов
/ 10 декабря 2010

Поскольку вы выполняете синтаксический анализ во время выполнения, а не во время компиляции, вы не можете выполнить откат системы типов Haskell (если только вы не импортируете соответствующие модули и не вызываете их вручную.)хочу обратиться к ML TAPL примеры проверки типов для простого лямбда-исчисления для вдохновения.http://www.cis.upenn.edu/~bcpierce/tapl/ (по реализации).Они делают немного больше, чем ваш синтаксический анализатор выражений, поскольку вы не поддерживаете лямбды.

...