Haskellの型レベル環境

Question

単純なDSLを実装するためにいくつかのHaskell拡張を使用しようとしています。私が望む機能は、変数の型レベルのコンテキストを持つことです。 私は、この種のものはAgdaやIdrisのような言語で一般的な場所であることを知っています。しかし、私はハスケルで同じ結果を達成することが可能かどうかを知りたいと思います。

私の考えは、タイプレベルの関連付けリストを使用することです。コードは以下の通りである：それは与えられた環境env上にある場合、変数にのみ使用することができることを確実にするために使用されるInモデルタイプレベルリストのメンバーシップの制約

{-# LANGUAGE GADTs, 
     DataKinds, 
     PolyKinds, 
     TypeOperators, 
     TypeFamilies, 
     ScopedTypeVariables, 
     ConstraintKinds, 
     UndecidableInstances #-} 

import Data.Proxy  
import Data.Singletons.Prelude 
import Data.Singletons.Prelude.List 

import GHC.Exts  
import GHC.TypeLits 

type family In (s :: Symbol)(a :: *)(env :: [(Symbol, *)]) :: Constraint where 
    In x t '[] =() 
    In x t ('(y,t) ': env) = (x ~ y , In x t env) 


data Exp (env :: [(Symbol, *)]) (a :: *) where 
    Pure :: a -> Exp env a 
    Map :: (a -> b) -> Exp env a -> Exp env b   
    App :: Exp env (a -> b) -> Exp env a -> Exp env b   
    Set :: (KnownSymbol s, In s t env) => proxy s -> t -> Exp env() 
    Get :: (KnownSymbol s, In s t env) => proxy s -> Exp env t 


test :: Exp '[ '("a", Bool), '("b", Char) ] Char 
test = Get (Proxy :: Proxy "b")   

タイプファミリー。私はGHCの7.10.3を使用してい

Could not deduce (In "b" Char '['("a", Bool), '("b", Char)]) 
    arising from a use of ‘Get’ 
In the expression: Get (Proxy :: Proxy "b") 
In an equation for ‘test’: test = Get (Proxy :: Proxy "b") 
Failed, modules loaded: Main. 

：

問題はGHCの制約ソルバーは、次のエラーメッセージを与えて、test機能に制約 In "b" Char [("a",Bool), ("b",Char)]を必要とすることはできないということです。どのように私はこれを解決することができますか、またはこれが不可能である理由の説明のヒントは非常に歓迎です。

Answer 1

Inは不可能な制約を生成します。

In "b" Char '['("a", Bool), '("b", Char)] = 
("b" ~ "a", ("b" ~ "b",()) 

それは一緒だと、それは全体的に不可能ですので、それは、不可能要素"a" ~ "b"を持っています。

さらに、私が仮定した値Charについては制約がありません。ルックアップ値です。

最も簡単な方法は、直接ルックアップ機能を使用することになります。

type family Lookup (s :: Symbol) (env :: [(Symbol, *)]) :: * where 
    Lookup s ('(s , v) ': env) = v 
    Lookup s ('(s' , v) ': env) = Lookup s env 

私たちは、ルックアップの種類に制約を置くためにLookup k xs ~ valを使用することができます。

また、Maybe *を返すこともできます。実際にはData.Singletons.Prelude.ListのLookupがそうしているので、それも使用できます。しかし、タイプ・レベルでは、部分的な関数を使用することがよくあります。タイプ・ファミリー・アプリケーションは、エラーをスローするのではなくスタックされているため、Lookup k xs :: *の値を持つことは、すでにkがxs 。

Answer 2

Inはあなたの考えではありません。実際はAllのようです。タイプIn x t xsの値は、（タイプ・レベル）リストの各要素が'(x,t)に等しいという証明です。自然数のようなより多くの種類である

data Elem x xs where 
    Here :: Elem x (x ': xs) 
    There :: Elem x xs -> Elem y (x ': xs) 

Elem：S (S Z)のそれとThere (There Here)の形状を比較

次GADTは、メンバーシップのより一般的な証拠です。あなたは、そのインデックスを与えることによって、アイテムがリストにあることを証明します。

ラムダ型の型チェッカーを書くために、Elemは、型の（タイプレベル）リストへのde Bruijn indexとして役に立ちます。あなたはおよそalpha-equivalenceを心配する必要はありません、彼らはシンプルだし、この例では、タイプレベルのルックアップテーブルまたはSymbolと周り混乱する必要はありません。

data Ty = NatTy | Ty ~> Ty 

data Term env ty where 
    Lit :: Nat -> Term env NatTy 
    Var :: Elem t env -> Term env t 
    Lam :: Term (u ': env) t -> Term env (u ~> t) 
    ($$) :: Term env (u ~> t) -> Term env u -> Term env t 

デBruijnグラフインデックスは、コンパイラの作家のための大きな利点を持っていますs。しかし、正しい考え方では、Bruijnインデックスを持つ言語でプログラムすることはありません。たとえタイプチェッカーを使っていてもそうです。これは、明示的な変数名で表面言語を翻訳するコンパイラの中間言語に適しています。

タイプレベル環境とde Bruijnインデックスはどちらも複雑なので、この言語のターゲットオーディエンスはですか？（および：はコストの価値があるタイプレベルの環境ですか？）親しみやすさ、シンプルさ、およびパフォーマンスが期待される組み込み型DSLですか？もしそうなら、higher-order abstract syntaxを使ってより深い埋め込みを考えてみましょう。それとも、それは中間の言語として使用されるのですか？それは、主な読者が自分自身、コンパイラの作家ですか？次に、Kmettのboundのようなライブラリを使用して、変数バインディングを処理し、とにかく起こる可能性があるため、型エラーの可能性を吸収します。タイプレベルの環境らの詳細について

、（私の知る限り）The View from the Leftため依存型付けプログラミング言語に埋め込まれた静的チェックラムダ計算型チェッカーの最初の例を参照。 Norellは同じプログラムのアガダ風味の展覧会にthe Agda tutorialとa series of lecturesを与えます。あなたのユースケースに関連すると思われるthis questionも参照してください。