小编com*_*mco的帖子

我只是开始玩idris和定理证明一般.我可以在互联网上关注大多数基本事实证据的例子,所以我想尝试一些我自己的任意事物.所以,我想为map的以下基本属性编写一个证明术语:

map : (a -> b) -> List a -> List b
prf : map id = id

直觉上,我可以想象证明应该如何工作:获取任意列表l并分析map id l的可能性.如果l是空的,那很明显; 当l非空时,它基于函数应用程序保持相等的概念.所以,我可以这样做:

prf' : (l : List a) -> map id l = id l

这就像一个所有声明.如何将其转化为所涉及功能相等的证明？

我想为树结构实现一个通用层次结构,以后可以用一种与实现无关的方式来描述树上的通用算法.

我从这个层次结构开始:

interface BinaryTree<Node> {
    Node left(Node);
    bool hasLeft(Node);

    Node right(Node);
    bool hasRight(Node);
}

interface BinaryTreeWithRoot<Node> : BinaryTree<Node> {
    Node root();
}

interface BinaryTreeWithParent<Node> : BinaryTree<Node> {
    Node parent(Node);
    bool hasParent(Node);
}

现在,基本上我希望能够以通用的方式实现子树的概念:对于每个类T:BinaryTree,我想要一个'类'子树(T),它提供相同的T功能(所以它必须来自它),并重写root()功能.

像这样的东西:

class Subtree<T, Node> : T, BinaryTreeWithRoot<Node> 
    where T : BinaryTree<Node>
{
    T reference;
    Node root;

    void setRoot(Node root) {
        this.root = root;
    }

    override Node BinaryTreeWithRoot<Node>::root() {
        return this.root;
    }

    // Now, inherit all the functionality of T, so an instance of this class can be …

我有以下代码:

sealed trait A

case class B[T](v: T) extends A
case class C[T](v: T) extends A

object Test {
  def swap(a: A): A = a match {
    case a: B[t] => C[t](a.v) // works!
    case C[t](v) => B[t](v) // error: C[t] does not take parameters
  }
}

我希望这两种情况都会失败,或者两种情况都会发生.第二种情况下错误的含义是什么？是否有语法解构参数化案例类？

注意:这里,小写't'是必不可少的.如果它是'T',则检查器将在方法的类型参数中查找它.

请考虑以下片段:

import Data.List

%default total

x : Elem 1 [1, 2]
x = Here

type : Type
type = Elem 1 [1, 2]

y : type
y = Here

这给出了错误:

检查y的右侧时:Elem x(x :: xs)(此处的类型)与iType(预期类型)之间的类型不匹配

y查询时的类型是:

type : Type
-----------
y : type

是否有可能type在类型归属期间或之前强制进行评估y,以便类型y为Elem 1 [1, 2]？

我的用例是我希望能够定义返回正确命题术语的通用谓词,例如:

subset : List a -> List a -> Type
subset xs ys = (e : a) -> Elem e xs -> Elem e ys …