6

一般的な質問

同じものを表す 2 つの異なる方法であるデータ型のペアがあります。1 つは String で変数名を記録し、もう 1 つは Int で変数名を記録します。現在、両方とも定義されています。ただし、ここでは最初の表現だけを説明したいと思います。2 つ目の表現は何らかの関係によって生成されます。

具体例

具体的には、最初のものは STLC ターム ユニバースのユーザー定義バージョンであり、2 つ目は同じものの de Bruijn インデックス付きバージョンです。

{-# LANGUAGE RankNTypes, GADTs, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeFamilies, UndecidableInstances, FunctionalDependencies, FlexibleInstances  #-} 


-- * Universe of Terms * -- 

data Term :: Type -> * where 
    Var :: Id -> Term a
    Lam :: Id -> Type -> Term b -> Term (a :-> b)
    App :: Term (a :-> b) -> Term a -> Term b 

    Let :: Id -> Term a -> Term b -> Term b 
    Tup :: Term a -> Term b -> Term (a :*: b)
    Lft :: Term a -> Term (a :+: b)
    Rgt :: Term b -> Term (a :+: b)

    Tru :: Term Boolean
    Fls :: Term Boolean
    Uni :: Term Unit

data TermIn :: Type -> * where 
    VarI :: Idx -> Info -> TermIn a 
    LamI :: Type -> TermIn b -> Info -> TermIn (a :-> b)
    AppI :: TermIn (a :-> b) -> TermIn a -> TermIn b

    LetI :: TermIn a -> TermIn b -> Info -> TermIn b   
    TupI :: TermIn a -> TermIn b -> TermIn (a :*: b)

    TruI :: TermIn Boolean
    FlsI :: TermIn Boolean
    UniI :: TermIn Unit

-- * Universe of Types * --

data Type 
    = Type :-> Type
    | Type :*: Type
    | Type :+: Type
    | Boolean
    | Unit
    | Void

-- * Synonyms * --

type Id   = String          -- * variable name
type Idx  = Int             -- * de-brujin's index
data Info = Rec Id String   -- * store original name and extra info

Termとに対して定義された関係が既に存在しTermInます:

    class DeBruijnPair a b | a -> b, b -> a where 
        decode  :: b -> a
        encode  :: a -> b

    instance DeBruijnPair (Term a) (TermIn a) where
        decode = undefined
        encode = undefined

Termの元の名前は に保存されているため、 とTermInの 1 対 1 のマッピングが存在することに注意してください。TermTermIn

質問を言い換える

Termこれでボイラー プレートがどれだけ関与しているかがわかります。これは、私が定義する洗練された抽象化と出力型に対する関数を使用して取り除きたいと考えていますTermIn。さらに多くのコンテキストを提供するために、さまざまなラムダ計算の定式化に対して、このような外部表現と de Bruijn 表現のペアを多数作成していますが、それらすべてに 1 対 1 の関係が成り立ちます。

4

1 に答える 1

6

Var最初のステップは、各表現 ( 、Lam、 )に固有の部分をLet残りの定義から分離することです。

data AbstractTerm ∷ Type → ★ where
    App ∷ AbstractTerm (a :-> b) → AbstractTerm a → AbstractTerm b

    Tup ∷ AbstractTerm a → AbstractTerm b → AbstractTerm (a :*: b)

    Lft ∷ AbstractTerm a → AbstractTerm (a :+: b)
    Rgt ∷ AbstractTerm b → AbstractTerm (a :+: b)

    Tru, Fls ∷ AbstractTerm Boolean

    Uni ∷ AbstractTerm Unit

data Term ∷ Type → ★ where 
    Var ∷ Id → Term a
    Lam ∷ Id → Type → Term b → Term (a :-> b) 
    Let ∷ Id → Term a → Term b → Term b 

data TermIn ∷ Type → ★ where 
    VarI ∷ Idx → Info → TermIn a 
    LamI ∷ Type → TermIn b → Info → TermIn (a :-> b)
    LetI ∷ TermIn a → TermIn b → Info → TermIn b

次に、「汎用」部分を必要な具体的な表現と組み合わせる必要があります。帰納的な定義を小さなチャンクに構築するためのよく知られたトリックがあります。データ型からの帰納的な呼び出しをリファクタリングし、サブ要素の型を型のパラメーターにします (この場合、型の種類に対する関数、オブジェクト言語の種類を追跡する必要があるため)。

data AbstractTerm (t ∷ Type → ★) ∷ Type → ★ where
    App ∷ t (a :-> b) → t a → AbstractTerm t b

    Tup ∷ t a → t b → AbstractTerm t (a :*: b)

    Lft ∷ t a → AbstractTerm t (a :+: b)
    Rgt ∷ t b → AbstractTerm t (a :+: b)

    Tru, Fls ∷ AbstractTerm t Boolean

    Uni ∷ AbstractTerm t Unit

data Term (t ∷ Type → ★) ∷ Type → ★ where 
    Var ∷ Id → Term t a
    Lam ∷ Id → Type → t b → Term t (a :-> b)
    Let ∷ Id → t a → t b → Term t b 

data TermIn (t ∷ Type → ★) ∷ Type → ★ where 
    VarI ∷ Idx → Info → TermIn t a 
    LamI ∷ Type → t b → Info → TermIn t (a :-> b)
    LetI ∷ t a → t b → Info → TermIn t b

この型をインスタンス化するには、抽象型と合計する誘導型定義を使用して、抽象型に渡すパラメーターを取得できます。

newtype ConcreteTermNamed ty
  = ConcreteTermNamed (Either (Term ConcreteTermNamed ty)
                              (AbstractTerm ConcreteTermNamed ty))

newtype ConcreteTermNameless ty
  = ConcreteTermNameless (Either (TermIn ConcreteTermNameless ty)
                                 (AbstractTerm ConcreteTermNameless ty))

これにより、各レベルで表現にとらわれない用語を使用するか、表現に固有の用語を使用するかを選択するためのノイズが少し追加され、さらに Haskell が義務付けた newtype ラッパーが必要になりますが、それ以外の場合は用語の言語はそのままになります。

var ∷ ConcreteTermNamed (Boolean :*: Unit)
var = ConcreteTermNamed
        (Right (Tup (ConcreteTermNamed (Left (Var "x")))
                    (ConcreteTermNamed (Left (Var "y")))))

fun ∷ ConcreteTermNamed (Boolean :-> (Unit :*: Boolean))
fun = ConcreteTermNamed (Left
        (Lam "b" Boolean
           (ConcreteTermNamed (Right
              (Tup (ConcreteTermNamed (Right Uni))
                   (ConcreteTermNamed (Left (Var "b"))))))))

このトリックは、任意の数の異なる帰納型を合計するために使用でき、より大きな言語をより小さく、よりモジュール化されたサブ言語に分解するためによく使用されます。たとえば、AbstractTerm をアプリケーション、製品、合計、および単位の各タイプにさらに分割し、それらを合計タイプに追加してすべてをマージするのは良いスタイルかもしれません。

于 2014-01-28T05:10:17.500 に答える