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 | Three
- data 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 True
- so是依赖于Bool的类型(or 索引,indexed over Bool)
- (我感觉这种编译器的依赖类型约束推理其实给程序员增加了额外的复杂性,不见得有多高明)
- data Vect: Nat -> Type -> Type where //Vect is indexed by Nat and parameterized by Type
- 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 = x
- plusSuc: (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 {
- intros
- rewrite (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
- > idris proof.idr
- 辅助C++类型设计?