5

Church エンコーディングを使用すると、組み込みの ADT システムを使用せずに、任意の代数データ型を表すことができます。たとえば、次のNatように表すことができます (Idris の例)。

-- Original type

data Nat : Type where
    natSucc : Nat -> Nat
    natZero : Nat

-- Lambda encoded representation

Nat : Type
Nat = (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat

natSucc : Nat -> Nat
natSucc pred n succ zero = succ (pred n succ zero)

natZero : Nat
natZero n succ zero = zero

Pair次のように表すことができます。

-- Original type
data Pair_ : (a : Type) -> (b : Type) -> Type where
    mkPair_ : (x:a) -> (y:b) -> Pair_ a b

-- Lambda encoded representation

Par : Type -> Type -> Type
Par a b = (t:Type) -> (a -> b -> t) -> t

pair : (ta : Type) -> (tb : Type) -> (a:ta) -> (b:tb) -> Par ta tb
pair ta tb a b k t = t a b

fst : (ta:Type) -> (tb:Type) -> Par ta tb -> ta
fst ta tb pair = pair ta (\ a, b => a)

snd : (ta:Type) -> (tb:Type) -> Par ta tb -> tb
snd ta tb pair = pair tb (\ a, b => b)

等々。さて、これらの型、コンストラクター、マッチャーを書くことは非常に機械的な作業です。私の質問は次のとおりです: ADT を型レベルの仕様として表現し、型自体 (つまりNat/ Par) と、それらの仕様から自動的にコンストラクター/デストラクタを派生させることは可能でしょうか? 同様に、これらの仕様を使用してジェネリックを導出できますか? 例：

NAT : ADT
NAT = ... some type level expression ...

Nat : Type
Nat = DeriveType NAT

natSucc : ConstructorType 0 NAT
natSucc = Constructor 0 NAT

natZero : ConstructorType 1 NAT
natZero = Constructor 1 NAT

natEq : EqType NAT
natEq = Eq NAT

natShow : ShowType NAT
natShow = Show NAT

... and so on
4

2 に答える 2

3

手始めに、多項式ファンクターを表す Idris コードをいくつか示します。

infix 10 |+|
infix 10 |*|

data Functor : Type where
  Rec : Functor
  Emb : Type -> Functor
  (|+|) : Functor -> Functor -> Functor
  (|*|) : Functor -> Functor -> Functor

LIST : Type -> Functor
LIST a = Emb Unit |+| (Emb a |*| Rec)

TUPLE2 : Type -> Type -> Functor
TUPLE2 a b = Emb a |*| Emb b

NAT : Functor
NAT = Rec |+| Emb Unit

以下は、それらの不動点のデータベースによる解釈です (詳細については、http ://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf の例 3.2 を参照してください) 。

adt : Functor -> Type -> Type
adt Rec t = t
adt (Emb a) _ = a
adt (f |+| g) t = Either (adt f t) (adt g t)
adt (f |*| g) t = (adt f t, adt g t)

data Mu : (F : Functor) -> Type where
  Fix : {F : Functor} -> adt F (Mu F) -> Mu F

そして、ここに教会の表現に基づく解釈があります：

Church : Functor -> Type
Church f = (t : Type) -> go f t t
  where
    go : Functor -> Type -> (Type -> Type)
    go Rec t = \r => t -> r
    go (Emb a) t = \r => a -> r
    go (f |+| g) t = \r => go f t r -> go g t r -> r
    go (f |*| g) t = go f t . go g t

だから私たちは例えばすることができます

-- Need the prime ticks because otherwise clashes with Nat, zero, succ from the Prelude...
Nat' : Type
Nat' = Mu NAT

zero' : Nat'
zero' = Fix (Right ())

succ' : Nat' -> Nat'
succ' n = Fix (Left n)

だけでなく、

zeroC : Church NAT
zeroC n succ zero = (zero ())

succC : Church NAT -> Church NAT
succC pred n succ zero = succ (pred n succ zero)
于 2016-06-29T03:01:40.683 に答える