Можно ли создать представление общих АТД на уровне типов?

Используя кодировку Черча, можно представить любой произвольный алгебраический тип данных без использования встроенной системы АТД. Например, Nat можно представить (пример в Идрисе) как:

-- 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)

И так далее. Теперь написание этих типов, конструкторов, сопоставителей — очень механическая задача. Мой вопрос: возможно ли представить АТД как спецификацию на уровне типа, а затем автоматически вывести сами типы (т. е. 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

functional-programming algebraic-data-types idris church-encoding agda
person MaiaVictor    schedule 28.06.2016    source источник
comment
Обратите внимание, что, насколько мне известно, в этих кодировках Черча отсутствуют зависимые исключения. Например. если Bool = (A : Type) -> A -> A -> A и tru,fls определены соответственно, вы не можете доказать (b: Bool) -> (b = tru \/ b = fls), в то время как вы могли бы с индуктивными типами.   -  person chi    schedule 28.06.2016
comment
Вы можете сделать это для гораздо более выразительной системы типов: полностью зависимые типы + индуктивные семейства. Производное Nat затем является элиминатором Nat = (P : Nat -> Type) -> (forall n. P n -> P (succ n)) -> P 0 -> forall n. P n. Я написал об этом сообщение в блоге. EqType также является производным (пример). Сколько типов вы хотите охватить? Только типы System F и никаких GADT?   -  person user3237465    schedule 28.06.2016
comment
@chi: действительно, похоже, это источник, подтверждающий ваше утверждение: Индукция не выводится в теории зависимых типов второго порядка   -  person Cactus    schedule 01.07.2016
comment
@Cactus, вы можете восстановить нейтрализаторы типов данных, закодированных в Церкви, с помощью внутренней параметризации. Однако отсутствуют ссылки.   -  person user3237465    schedule 01.07.2016

Ответы (2)


arrow_upward
6
arrow_downward

Индексированные описания не сложнее, чем полиномиальные функторы. Рассмотрим эту простую форму пропозициональных описаний:

data Desc (I : Set) : Set₁ where
  ret : I -> Desc I
  π   : (A : Set) -> (A -> Desc I) -> Desc I
  _⊕_ : Desc I -> Desc I -> Desc I
  ind : I -> Desc I -> Desc I

π похоже на Emb, за которым следует |*|, но позволяет остальной части описания зависеть от значения типа A. _⊕_ это то же самое, что и |+|. ind похоже на Rec, за которым следует |*|, но он также получает индекс будущего подтермина. ret завершает описание и указывает индекс построенного термина. Вот непосредственный пример:

vec : Set -> Desc ℕ
vec A = ret 0
      ⊕ π ℕ λ n -> π A λ _ -> ind n $ ret (suc n)

Первый конструктор vec не содержит никаких данных и строит вектор длины 0, поэтому мы ставим ret 0. Второй конструктор получает длину (n) подвектора, некоторый элемент типа A и подвектор и строит вектор длины suc n.

Построение неподвижных точек описаний аналогично построению полиномиальных функторов.

⟦_⟧ : ∀ {I} -> Desc I -> (I -> Set) -> I -> Set
⟦ ret i   ⟧ B j = i ≡ j
⟦ π A D   ⟧ B j = ∃ λ x -> ⟦ D x ⟧ B j
⟦ D ⊕ E   ⟧ B j = ⟦ D ⟧ B j ⊎ ⟦ E ⟧ B j
⟦ ind i D ⟧ B j = B i × ⟦ D ⟧ B j

data μ {I} (D : Desc I) j : Set where
  node : ⟦ D ⟧ (μ D) j -> μ D j

Vec просто

Vec : Set -> ℕ -> Set
Vec A = μ (vec A)

Раньше это было adt Rec t = t, но теперь термины индексируются, поэтому t тоже индексируется (выше он называется B). ind i D содержит индекс подтермина i, к которому затем применяется μ D. Таким образом, при интерпретации второго конструктора векторов Vec A применяется к длине подвектора n (из ind n $ ...), таким образом, подтерм имеет тип Vec A n.

В последнем случае ret i требуется, чтобы построенный термин имел тот же индекс (i), что и ожидалось (j).

Получение элиминаторов для таких типов данных немного сложнее:

Elim : ∀ {I B} -> (∀ {i} -> B i -> Set) -> (D : Desc I) -> (∀ {j} -> ⟦ D ⟧ B j -> B j) -> Set
Elim C (ret i)   k = C (k refl)
Elim C (π A D)   k = ∀ x -> Elim C (D x) (k ∘ _,_ x)
Elim C (D ⊕ E)   k = Elim C D (k ∘ inj₁) × Elim C E (k ∘ inj₂)
Elim C (ind i D) k = ∀ {y} -> C y -> Elim C D (k ∘ _,_ y)

module _ {I} {D₀ : Desc I} (P : ∀ {j} -> μ D₀ j -> Set) (f₀ : Elim P D₀ node) where
  mutual
    elimSem : ∀ {j}
            -> (D : Desc I) {k : ∀ {j} -> ⟦ D ⟧ (μ D₀) j -> μ D₀ j}
            -> Elim P D k
            -> (e : ⟦ D ⟧ (μ D₀) j)
            -> P (k e)
    elimSem (ret i)    z       refl    = z
    elimSem (π A D)    f      (x , e)  = elimSem (D x) (f  x) e
    elimSem (D ⊕ E)   (f , g) (inj₁ x) = elimSem D f x
    elimSem (D ⊕ E)   (f , g) (inj₂ y) = elimSem E g y
    elimSem (ind i D)  f      (d , e)  = elimSem D (f (elim d)) e

    elim : ∀ {j} -> (d : μ D₀ j) -> P d
    elim (node e) = elimSem D₀ f₀ e

Подробности я подробно изложил в другом месте.

Его можно использовать следующим образом:

elimVec : ∀ {n A}
        -> (P : ∀ {n} -> Vec A n -> Set)
        -> (∀ {n} x {xs : Vec A n} -> P xs -> P (x ∷ xs))
        -> P []
        -> (xs : Vec A n)
        -> P xs
elimVec P f z = elim P (z , λ _ -> f)

Получение разрешимого равенства более многословно, но не сложнее: нужно просто потребовать, чтобы каждое Set, которое получает π, имело разрешимое равенство. Если все нерекурсивное содержимое вашего типа данных имеет разрешимое равенство, то и ваш тип данных также имеет его.

Код.

person user3237465    schedule 30.06.2016

arrow_upward
3
arrow_downward

Для начала приведем код Идриса, представляющий полиномиальные функторы:

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

Вот основанная на данных интерпретация их фиксированных точек (см., например, 3.2 в http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf для получения дополнительной информации)

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)
person Cactus    schedule 29.06.2016
comment
Можно ли это распространить за пределы неподвижных точек полиномиальных функторов? например. используя описания? - person Benjamin Hodgson♦; 29.06.2016
comment
Проницательно и гораздо проще, чем я думал. Во-вторых, я бы хотел, чтобы это было расширено, чтобы объяснять описания простыми словами. - person MaiaVictor; 29.06.2016
comment
@ Бенджамин Ходжсон, я добавил ответ, связанный с описаниями. - person user3237465; 30.06.2016