ГАДТ для полиморфного списка - PullRequest
Новая
       4

ГАДТ для полиморфного списка

5 голосов
/ 20 января 2012

Я анализирую несколько операторов вида 

v1 = expression1
v2 = expression2
...

Я использую монаду состояния, и мое состояние должно быть парой (String, Expr a), я действительно настаиваю на том, чтобы выражения были напечатаны,Я попытался реализовать состояние как [PPair], где я определяю PPair с помощью GADT: 

data PPair where
    PPair :: (String, Expr a) -> PPair

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

evalVar k ((PPair (kk, v)):s) = if k == kk then v else evalVar k s

Я получаю: 

Inferred type is less polymorphic than expected

, что вполне ожидаемо.Как мне обойти эту проблему?Я знаю, что могу решить эту проблему, разбив тип на все типы-кандидаты a, но нет ли более аккуратного пути?

1 Ответ

9 голосов
/ 20 января 2012

Проблема в том, что нет возможного типа evalVar, который может иметь: 

evalVar :: String -> [PPair] -> Expr ?

Нельзя сказать, что ? - это a, потому что тогда вы утверждаете, что возвращаемое значение работает для любого значения a. Однако вы можете заключить «1010 * с неизвестным типом» в собственный тип данных: 

data SomeExpr where
  SomeExpr :: Expr a -> SomeExpr

или, что то же самое, с RankNTypes вместо GADTs: 

data SomeExpr = forall a. SomeExpr (Expr a)

Это называется экзистенциальная квантификация . Затем вы можете переписать PPair, используя SomeExpr: 

data PPair = PPair String SomeExpr

и evalVar получается: 

evalVar k (PPair kk v : xs)
  | k == kk = v
  | otherwise = evalVar k xs

(Конечно, вместо этого вы могли бы использовать [(String,SomeExpr)] и стандартную функцию lookup.)

В общем, попытка сохранить выражения полностью напечатанными на уровне Хаскелла, как это, вероятно, бесполезное упражнение; язык с зависимой типизацией, такой как Agda , не будет иметь с этим проблем, но вы, вероятно, в конечном итоге столкнетесь с чем-то, что Haskell не может сделать довольно быстро, или ослабите вещи до такой степени, что безопасность во время компиляции вы хотели из усилия потеряно.

Нельзя сказать, что это никогда не работает, конечно; Типизированные языки были одним из мотивирующих примеров для ГАДЦ. Но это может работать не так, как вы хотите, и вы, вероятно, столкнетесь с проблемами, если ваш язык имеет какие-то нетривиальные функции системы типов, такие как полиморфизм.

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

data PPair where
  PPair :: Var a -> Expr a -> PPair

evalVar :: Var a -> [PPair] -> Maybe (Expr a)

Хороший способ добиться чего-то похожего на это - использовать пакет vault ; вы можете создать Key s из ST и IO и использовать Vault в качестве гетерогенного контейнера. В основном это похоже на Map, где ключи содержат тип соответствующего значения. В частности, я бы предложил определить Var a как Key (Expr a) и использовать Vault вместо вашего [PPair]. (Полное раскрытие: я работал над пакетом хранилища.)

Конечно, вам все равно придется сопоставлять имена переменных со значениями Key, но вы можете создать все Key сразу после разбора и переносить их вместо строк. (Однако было бы немного потрудиться перейти от Var к соответствующему имени переменной с помощью этой стратегии; вы можете сделать это с помощью списка экзистенциалов, но решение слишком длинное, чтобы вставить этот ответ.)

(Кстати, вы можете иметь несколько аргументов для конструктора данных с помощью GADT, как и обычные типы: data PPair where PPair :: String -> Expr a -> PPair.)

...