小编永劫回*_*劫回帰的帖子

我试图在矢量上定义rev函数，它的大小嵌入其中，但我不知道如何在其上定义rev函数。

这是我的类型定义：

Inductive vect {X : Type} : nat -> Type -> Type
  := Nil  : vect 0 X
   | Cons : forall n, X -> vect n X -> vect (S n) X
.

我已经定义了一些有用的功能：

Fixpoint app {X : Type} {n m : nat} (v1 : vect n X) (v2 : vect m X)
: vect (n + m) X :=
  match v1 with
    | Nil => v2
    | Cons _ x xs => Cons _ x (app xs …

我有一个在类内声明的对象A，我想在初始化对象B时初始化对象A：

class A{
    private:
        int num1;
        string word;
    public:
        A(int,word);
};

A::A(int _num1, string _word){
    num1 = num1;
    word = _word;
}

class B{
    private:
        char letter;
        A a;
    public:
        B(char,int,string)
};

B::B(char _letter, int _num1, string _word){
    letter = _letter;
    a(_num1, _word);
}

这给出了错误：只能调用一个函数。我的问题是，我如何在另一个对象内部拥有一个可以由外部对象构造函数初始化的对象。

我正在阅读文章使用 Conor McBride和Ross Paterson的效果进行Applcative编程,我无法弄清楚为什么他们的第一段代码类型检查.(我有强大的OCaml背景和弱的haskell背景).

有一个函数ap来自Control.Monad以下类型:

ap :: Monad m => m (a -> b) -> m a -> m b

这个函数很容易写成这样:

ap mf mx = do { f <- mf ; x <- mx ; return (f x) }

然后他们写下以下内容:

sequence :: [IO a] ? IO [a]
sequence [] = return []
sequence (c : cs) = return (:) `ap` c `ap` sequence cs

我的问题是我无法弄清楚如何计算(:) `ap` c `ap` sequence cs手工类型,因为它的类型(:) …