Haskellの異種リストの型安全な参照の詳細

Question

Haskellで依存型プログラミングを面白くしようとしています。より具体的には、型セーフな検索操作です。

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

と私は答え持っている：Previouslyは、私は次のデータ型のルックアップ操作を実装する方法について尋ねてきました

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によって表される：これらのデータ型を使用して

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) 

、：

{-# 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 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 

：私は存在量化（タイプEx2）のいくつかの並べ替えを使用してルックアップ関数を定義します、 とても良い。いくつかの面白い問題が発生しました：

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コンテキストを使用して、それはFAこの最後の、weaken INGのステップであると私には思えますなぜなら、Lookup s ctx ~ Nothingは、weaken（あなたがシャドーイングの問題ではないことを知っているのでコンテキストをシフトすることができます）に必要なものをGHCが証明するのに十分な構造を持っていないからです。