是否有可能在结构演算中表达平衡的未标记二叉树的类型？

Question

我试图通过Morte项目探索和理解建筑微积分的领域.我知道可以在Agda中表示这样的数据类型,但是对于我来说如何在这样的极简主义环境中表示它并不明显.怎么可能这样呢？我的意思是这个数据类型,在Idris中:

data Tree : Nat -> Type -> Type where
    Leaf : a -> Tree Z a
    (::) : Tree k a -> Tree k a -> Tree (S k) a

Answer 1

我不知道Morte的细节,但我有一些关于更广泛的类型lambda-calculi可行的线索.

如果Nat以不可预测的方式定义,则可以通过迭代来定义这些树.

Nat : *
Nat = (x : *) -> (x -> x) -> x -> x
Pair : * -> * -> *
Pair x y = (z : *) -> (x -> y -> z) -> z
Tree : * -> Nat -> *
Tree a n = n * (\ t -> Pair t t) a

当然,为了逃避这一点,我需要大量淘汰.在这里,我随便采取了* : *,但这一般不安全.归纳定义可以毫无疑问地允许大量消除:不可预测编码的数据类型,而不是这样.

但是,在上面,我利用了这样一个事实,即树的索引结构恰好与Nat索引它们的索引结构兼容,并且没有理由说一般情况下应该是这种情况.指数各种各样古怪的方式各不相同:只有那些表征某种"大小"的人才会越来越小.

索引结构确实允许教会编码的演示文稿.只是不是迭代一个集合,而是迭代一个索引集.这是表达它的一种方式.

Tree : * -> Nat -> *
Tree a n = (x : Nat -> *) ->
           (a -> x Z) ->
           ((n : Nat) -> x n -> x n -> x (S n)) ->
           x n

写一些像这样的东西很容易

leftmost : (a : *) -> (n : Nat) -> Tree a n -> a
leftmost a n t = t (\ _ -> a) (\ a -> a) (\ _ l _ -> l)

但

leftChild : (a : *) -> (n : Nat) -> Tree a (S n) -> Tree a n

是一个更高的订单,需要一些方法来检查或约束数字.这就是为什么GHC Haskell拥有所有关于平等的东西~.