Как представить список конструкторов переменной типа с помощью GADT? - PullRequest
Новая
       9

Как представить список конструкторов переменной типа с помощью GADT?

0 голосов
/ 03 декабря 2018

Я внедряю небольшой DSL для исследовательского проекта, с которым я связан.Поскольку это пример буквально каждого объяснения GADT, я решил, что сейчас самое время начать их использовать.Очевидные выражения (арифметика и т. Д.) Работали нормально, но мой DSL должен поддерживать пользовательские функции, и именно здесь я столкнулся с проблемой.

Без GADT структура моего типа выражения выглядела нескольковот так (сокращенно до минимального примера): 

data Expr = IntConst Int
          | BoolConst Bool
          | Plus Expr Expr
          | Times Expr Expr -- etc
          | AndAlso Expr Expr -- etc
          | Call String [Expr] -- function call!

Если преобразовать в GADT, как я могу выразить правило Call? 

data Expr a where
     IntConst :: Int -> Expr Int
     BoolConst :: Bool -> Expr Bool
     Plus :: Expr Int -> Expr Int -> Expr Int
     Times :: Expr Int -> Expr Int -> Expr Int
     AndAlso :: Expr Bool -> Expr Bool -> Expr Bool
     Call :: ???

Сначала я подумал, что это невозможнобез некоторых супер причудливых зависимых типов, потому что нет никакого способа узнать, какие типы будет принимать данная пользовательская функция (также тип возвращаемого значения, но я могу это исправить, сделав Call return Expr a и специализируясь на строительной площадке).Я могу принудить его к проверке типов, «стерев» тип, добавив правила 

     EraseInt :: Expr Int -> Expr a
     EraseBool :: Expr Bool -> Expr a

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

Справка?

Ответы [ 2 ]

0 голосов
/ 03 декабря 2018

Возможно, вам не нужно идти зависимым маршрутом для того, что вы хотите.Как насчет решения, в котором вы разделяете как построение, так и вызов функций.Это позволяет вам набирать ваши функции при их создании, поэтому вы можете иметь вызовы с проверкой типа. 

data Expr a where
     IntConst  :: Int -> Expr Int
     BoolConst :: Bool -> Expr Bool
     Plus      :: Expr Int -> Expr Int -> Expr Int
     Times     :: Expr Int -> Expr Int -> Expr Int
     AndAlso   :: Expr Bool -> Expr Bool -> Expr Bool
     Fun       :: String -> Expr (a->b)
     Call      :: Expr (a->b) -> Expr a -> Expr b

-- type checks
test = Call (Fun "f" :: Expr (Int -> Int)) (IntConst 1)

-- doesn't type check
test' = Call (Fun "f" :: Expr (Int -> Int)) (BoolConst False)

Для функций с несколькими аргументами вы можете работать в режиме карри с несколькими вызовами, то есть 

 Call (Call (Fun "f" :: Expr (Int->Int->Int)) (IntConst 1)) (IntConst 1)

Или вы можете реализовать кортежи на вашем языке.

0 голосов
/ 03 декабря 2018

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

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE TypeOperators   #-}
{-# LANGUAGE PatternSynonyms #-}

data ArgList (as :: [*]) where
  NilArgList :: ArgList '[]
  ConsArg    :: Expr a -> ArgList as -> ArgList (a ': as)

data Expr a where
  IntConst  :: Int -> Expr Int
  BoolConst :: Bool -> Expr Bool
  Plus      :: Expr Int -> Expr Int -> Expr Int
  Times     :: Expr Int -> Expr Int -> Expr Int
  AndAlso   :: Expr Bool -> Expr Bool -> Expr Bool
  Call      :: String -> ArgList as -> Expr b

pattern x :^ y = ConsArg x y
infixr :^

example :: Expr Int
example =
  Call "exampleFn" (IntConst 1 :^ BoolConst True :^ NilArgList
                        :: ArgList [Int, Bool])

Вам нужно будет указать некоторые явные сигнатуры типов для списков аргументов (как в example).Кроме того, тип результата Call (forall b. Expr b) немного неудобен, но я не уверен, что этого можно избежать, если у вас больше информации о типе, чем String для функции, которую он принимает. Если у вас было большетам вы также можете связать типы аргументов (as) с ожидаемыми типами аргументов для функции.Я думаю, что нам нужно больше подробностей о конкретной ситуации, которую вы должны пройти дальше с этой частью.

...