Seven More Languages in Seven Weeks （读书笔记）：Idris

Idris

Day 1
基本上还是Haskell的语法？
*functions> :t map
Prelude.Functor.map : Functor f => (a -> b) -> (f a) -> f b
map (\x => x * 0.5) (the (List Float) [3.14, 2.78])
数据类型：idris/day1/data_types.idr
data DumbNumber = Naught | One | Two | Threedata MyList a = Blank | (::) a (MyList a)
data Maybe a = Nothing | Just a

Day 2：Dependent Types？（对value施加更多的约束）
data Vect : Nat -> Type -> Type where //Vect is indexed by Nat and parameterized by Type
Nil : Vect Z a(::) : a -> Vect k a -> Vect (S k) a(++) : Vect n a -> Vect m a -> Vect (n + m) a //新的类型声明
data so : Bool -> Type where
oh : so Trueso是依赖于Bool的类型（or 索引，indexed over Bool）
（我感觉这种编译器的依赖类型约束推理其实给程序员增加了额外的复杂性，不见得有多高明）

Day 3
> idris proof.idr
*proof> :e
show plus x y等于plus y x（加法交换律）：
plus Zero y = plus y Zero
If plus x y = plus y x , then plus (Suc x) y = plus y (Suc x)

proof.idr：
plusZero : (x : Natural) -> plus x Zero = xplusSuc : (x : Natural) -> (y : Natural) -> Suc (plus x y) = plus x (Suc y)
Idris> :l proof.idr
*proof> :m*proof> :p plusCommutes_0_y-Proof.plusCommutes_0_y> intros（称为策略？）-Proof.plusCommutes_0_y> rewrite (plusZero y)-Proof.plusCommutes_0_y> trivial-Proof.plusCommutes_0_y> qed
总结：plusCommutes_0_y = proof {
introsrewrite (plusZero y)trivial}
接下来，*proof> :p plusCommutes_Sx_y
-Proof.plusCommutes_Sx_y> intros-Proof.plusCommutes_Sx_y> rewrite (plusSuc y x)定义hypothesis变量：plusCommutes (Suc x) y = let hypothesis = plusCommutes x y in ?plusCommutes_Sx_y-Proof.plusCommutes_Sx_y> rewrite hypothesis-Proof.plusCommutes_Sx_y> trivial-Proof.plusCommutes_Sx_y> qed

辅助C++类型设计？