受this blog post和this code的启发我以为我会在Idris中使用它的接口（类型类）尝试一些类别理论。 我定义Category如下，工作正常： interface Category (obj : Type) (hom : obj -> obj -> Type) where
id : {a : obj} -> hom a a
comp : {a, b, c :
我试图实现尽可能多的系统F（多态lambda微积分），因为我可以在伊德里斯。现在我面对，我想用一个例子来说明一个问题： data Foo = Bar Nat
Eq Foo where
(Bar _) == (Bar _) = True
data Baz: Foo -> Type where
Quux: (n: Nat) -> Baz (Bar n)
Eq (Baz f) where
我想证明一些简单的事情与idris，但我失败悲惨。这里是我的代码 module MyReverse
%hide reverse
%default total
reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = reverse xs ++ [x]
listEmptyAppend : (l : List a) -
使用Church编码，可以在不使用内置ADT系统的情况下表示任何任意代数数据类型。例如，Nat可以表示（在伊德里斯例如）为： -- Original type
data Nat : Type where
natSucc : Nat -> Nat
natZero : Nat
-- Lambda encoded representation
Nat : Type
Na
我与伊德里斯最近很多实验，并与下面的“一组类型级别定义”上来： mutual
data Set : Type -> Type where
Empty : Set a
Insert : (x : a) -> (xs : Set a) -> Not (Elem x xs) -> Set a
data Elem : (x : a) -> Set a -> Typ