Подробнее о типе безопасного поиска для гетерогенных списков в Haskell

Question

Я пытаюсь немного повеселиться с навязчивым программированием в Haskell, более конкретно с типом безопасного поиска. Previously, я спросил о том, как осуществить операцию подстановки для следующих типов данных:

data Attr (xs :: [(Symbol,*)]) where 
    Nil :: Attr '[] 
    (:*) :: (Sing s, t) -> Attr xs -> Attr ('(s , t) ': xs) 

И я получил ответ:

lookupAttr :: (Lookup s env ~ 'Just t) => Sing s -> Attr env -> t 
lookupAttr s ((s', t) :* env') = case s %:== s' of 
    STrue -> t 
    SFalse -> lookupAttr s env' 

Это работает отлично. Теперь я хочу, чтобы определить гетерогенный список значений типизированного синтаксиса, представленный типом Exp:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators, PolyKinds #-} 
import Data.Singletons.Prelude.List 
import Data.Singletons.Prelude.Bool 
import Data.Singletons.Prelude.Eq 

data Exp (env :: [(Symbol,*)]) :: * -> * where 
    Value :: String -> Exp env String 
    Var :: (Lookup s env ~ 'Just t) => Sing s -> Exp env t 
    Op :: Exp env t -> Exp env t -> Exp env t 

гетерогенный тип списка определяется по типу Env данных:

data Env (env :: [(Symbol,*)]) where 
    Nil :: Env '[] 
    Cons :: (Lookup s' env ~ 'Nothing) => 
     (Sing s' , 
      Exp ('(s', a) ': env) a) -> 
     Env env -> 
     Env ('(s',a) ': env) 

Используя эти типы данных, Я определяю функцию просмотра с помощью какого-то экзистенциальной квантификации (типа Ex2):

data Ex2 (p :: k -> k' -> *) where 
    Ex2 :: p e i -> Ex2 p 

lookupEnv :: Lookup s env ~ 'Just t => Sing s -> Env env -> Ex2 Exp 
lookupEnv s (Cons (s',e) env) 
    = case s %:== s' of 
     STrue -> Ex2 e 
     SFalse -> lookupEnv s env 

до сих пор , так хорошо. Теперь я прихожу к некоторым интересным проблемам:

1) Есть ли способ определить lookupEnv без использования этого вида экзистенциальной количественной оценки, предоставляемой по типу Ex2?

2) Предположим, что я хочу определить операцию для изменения позиции ввода в значение типа Env. Очевидная попытка определить эту функцию является

modifyEnv :: Lookup s env ~ 'Just t => Sing s -> Exp env t -> Env env -> Env env 
modifyEnv s e (Cons (s',e') env') 
    = case s %:== s' of 
      STrue -> Cons (s', Op e e') env' 
      SFalse -> Cons (s',e') (modifyEnv s e env') 

Функция modifyEnv составить некоторое выражение с другим в окружающей среде. Эта функция не принимается GHC, которая возвращает загадочное сообщение об ошибке. Как я могу определить такую ​​функцию модификации?

Answer 1

Я понимаю, что это не полное решение, потому что оно не использует гладкость Symbol-indexed Env, но это может дать вам хорошую отправную точку. Я использую «типизированной де индекса Брейна в контексте» типа вместо:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators #-} 

data Var (ctx :: [*]) :: * -> * where 
    Here :: Var (a ': ctx) a 
    There :: Var ctx a -> Var (b ': ctx) a 

data Exp (ctx :: [*]) :: * -> * where 
    Value :: String -> Exp ctx String 
    Var :: Var ctx t -> Exp ctx t 
    Op :: Exp ctx t -> Exp ctx t -> Exp ctx t 

data Env (ctx :: [*]) where 
    Nil :: Env '[] 
    Cons :: Exp (a ': ctx) a -> Env ctx -> Env (a ': ctx) 

Это позволяет писать версию набранного из lookupEnv, например, так:

lookupEnv :: Env ctx -> Var ctx t -> Exp ctx t 
lookupEnv (Cons e env) v = case v of 
    Here -> e 
    There v -> weaken $ lookupEnv env v 

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

weaken :: Exp ctx t -> Exp (a ': ctx) t 
weaken (Value s) = Value s 
weaken (Var v) = Var (There v) 
weaken (Op f e) = Op (weaken f) (weaken e) 

мне кажется, что с помощью Symbol -indexed контекстов, это последний, weaken ИНГ шага, метрономы ils, потому что Lookup s ctx ~ Nothing, похоже, не имеет достаточной структуры для GHC, чтобы доказать, что вам нужно для weaken (что вы можете перенести контекст, так как вы знаете, что проблема не будет скрыта).