有關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

我意識到這不是一個完整的解決方案，因爲它沒有使用索引諷刺，但它可能會給你一個很好的起點。我使用的是「類型的德布魯因索引上下文」類型，而不是：

{-# 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（您可以改變上下文，因爲您知道不存在影子問題）。