Можно ли гарантировать, что две переменные типа GADT одинаковы без зависимых типов? - PullRequest
Новая
       36

Можно ли гарантировать, что две переменные типа GADT одинаковы без зависимых типов?

0 голосов
/ 21 мая 2018

Я пишу компилятор, в котором я использую GADT для своего IR, но стандартные типы данных для всего остального.У меня возникают проблемы при преобразовании старого типа данных в GADT.Я попытался воссоздать ситуацию с меньшим / упрощенным языком ниже.

Для начала у меня есть следующие типы данных: 

data OldLVal = VarOL Int -- The nth variable. Can be used to construct a Temp later.
             | LDeref OldLVal

data Exp = Var Int -- See above
         | IntT Int32
         | Deref Exp

data Statement = AssignStmt OldLVal Exp
               | ...

Я хочу преобразовать их в этот промежуточныйform: 

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

-- Note: this is a Phantom type
data Temp a = Temp Int

data Type = IntT
          | PtrT Type

data Command where
    Assign :: NewLVal a -> Pure a -> Command
    ...

data NewLVal :: Type -> * where
    VarNL :: Temp a -> NewLVal a
    DerefNL :: NewLVal ('PtrT ('Just a)) -> NewLVal a

data Pure :: Type -> * where
    ConstP :: Int32 -> Pure 'IntT
    ConstPtrP :: Int32 -> Pure ('PtrT a)
    VarP :: Temp a -> Pure a

На данный момент я просто хочу написать преобразование из старого типа данных в новый GADT.Сейчас у меня есть нечто, похожее на это. 

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
   newLval <- convertLVal oldLval -- Either String (NewLVal a)
   pure <- convertPure exp -- Either String (Pure b)
   -- return $ Assign newLval pure -- Obvious failure. Can't ensure a ~ b.
   pure' <- matchType newLval pure -- Either String (Pure a)
   return $ Assign newLval pure'

-- Converts Pure b into Pure a. Should essentially be a noop, but simply 
-- proves that it is possible.
matchType :: NewLVal a -> Pure b -> Either String (Pure a)
matchType = undefined

Я понял, что не могу написать convert тривиально, поэтому я попытался решить проблему, используя эту идею matchType, которая действуеткак доказательство того, что эти два типа действительно равны.Вопрос в том, как мне написать matchType?Это было бы намного проще, если бы у меня были полностью зависимые типы (или мне так сказали), но могу ли я закончить этот код здесь?

Альтернативой этому было бы как-то предоставить newLval в качестве аргументаconvertPure, но я думаю, что по сути просто пытается использовать зависимые типы.

Любые другие предложения приветствуются.

Если это поможет, у меня также есть функция, которая может преобразовать Exp или OldLVal для его типа: 

class Typed a where
    typeOf :: a -> Type
instance Typed Exp where
    ...
instance Typed OldLVal where
    ...

РЕДАКТИРОВАТЬ:

Благодаря превосходным ответам ниже, я смог закончить написание этого модуля.

В итоге я использовал пакет singletons , упомянутый ниже.Сначала это было немного странно, но я нашел, что это довольно разумно использовать после того, как я начал понимать, что я делаю.Однако я столкнулся с одной ловушкой: для типов convertLVal и convertPure требуется экзистенциал для выражения. 

data WrappedPure = forall a. WrappedPure (Pure a, SType a)
data WrappedLVal = forall a. WrappedLVal (NewLVal a, SType a)

convertPure :: Exp -> Either String WrappedPure
convertLVal :: OldLVal -> Either String WrappedLVal

Это означает, что вам придется развернуть этот экзистенциал в convert,но в остальном ответы ниже укажут вам путь.Большое спасибо еще раз.

Ответы [ 2 ]

0 голосов
/ 21 мая 2018

Вы хотите выполнить сравнение во время выполнения для некоторых данных уровня типа (а именно Type s, по которым индексируются ваши значения).Но к тому времени, когда вы запустите свой код, и значения начнут взаимодействовать, типы уже давно исчезнут.Они стираются компилятором во имя создания эффективного кода.Поэтому вам нужно вручную восстановить данные уровня типа, которые были стерты, используя значение, которое напоминает вам о типе, который вы забыли, на который вы смотрели.Вам нужна singleton копия Type. 

data SType t where
    SIntT :: SType IntT
    SPtrT :: SType t -> SType (PtrT t)

Члены SType выглядят как члены Type - сравните структуру значения, подобного SPtrT (SPtrT SIntT), с этимиз PtrT (PtrT IntT) - но они индексируются по (тип-уровню) Type s, на которые они похожи.Для каждого t :: Type есть ровно один SType t (отсюда и название singleton ), и поскольку SType является GADT, сопоставление с шаблоном в SType t сообщает контролеру типов о t.Синглтоны охватывают строгое принудительное разделение между типами и значениями.

Поэтому, когда вы создаете свое типизированное дерево, вам нужно отслеживать время выполнения SType s ваших значений и сравнивать их при необходимости.(В основном это означает написание частично проверенного средства проверки типов.) В Data.Type.Equality есть класс , содержащий функцию, которая сравнивает два синглета и сообщает вам, совпадают ли их индексы. 

instance TestEquality SType where
    -- testEquality :: SType t1 -> SType t2 -> Maybe (t1 :~: t2)
    testEquality SIntT SIntT = Just Refl
    testEquality (SPtrT t1) (SPtrT t2)
        | Just Refl <- testEquality t1 t2 = Just Refl
    testEquality _ _ = Nothing

Применение этого в вашей функции convert выглядит примерно так: 

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
    (newLval, newLValSType) <- convertLVal oldLval
    (pure, pureSType) <- convertPure exp
    case testEquality newLValSType pureSType of
        Just Refl -> return $ Assign newLval pure'
        Nothing -> Left "type mismatch"

На самом деле не так уж много программ с зависимой типизацией, которые вы не можете подделать с помощью TypeInType, иесть ли что-нибудь?), но очень сложно дублировать все ваши типы данных как в «нормальной», так и в «одиночной» форме.(Дублирование становится еще хуже, если вы хотите неявно передавать синглтоны - подробнее см. Хасохизм .) Пакет singletons может генерировать большую частьшаблон для вас, но это на самом деле не облегчает боль, вызванную дублированием самих понятий.Вот почему люди хотят добавить в Haskell реальные зависимые типы, но до этого еще далеко.

Новый Type.Reflection модуль содержит переписанный класс Typeable,Его TypeRep подобен GADT и может выступать в качестве своего рода «универсального синглтона».Но, на мой взгляд, программирование с ним даже более неловко, чем программирование с помощью синглетонов.

0 голосов
/ 21 мая 2018

matchType как написано невозможно реализовать, но идея, к которой вы стремитесь, определенно возможна.Вы знаете о Data.Typeable?Typeable - это класс, который предоставляет некоторые основные отражающие операции для проверки типов.Чтобы использовать его, вам нужно ограничение Typeable a в области видимости для любой переменной типа a, о которой вы хотите знать.Так что для matchType у вас будет 

matchType :: (Typeable a, Typeable b) => NewLVal a -> Pure b -> Either String (Pure a)

Также необходимо заражать ваши GADT каждый раз, когда вы хотите скрыть переменную типа: 

data Command where
    Assign :: (Typeable a) => NewLVal a -> Pure a -> Command
    ...

Но если у вас есть соответствующие ограниченияв области видимости вы можете использовать eqT для сравнения типов во время выполнения.Например 

-- using ScopedTypeVariables and TypeApplications
matchType :: forall a b. (Typeable a, Typeable b) => NewLVal a -> Pure b -> Either String (Pure b)
matchType = case eqT @a @b of
                Nothing -> Left "types are not equal"
                Just Refl -> {- in this scope the compiler knows that
                                a and b are the same type -}
...