Re:The Power of Ten – Rules for Developing Safety Critical Code
by icen on Thursday July 14, 2016 @08:54AM
(#12093290)
An expressive and ergonomic type system goes a very long way into codifying that intent.
For example, it's quite obvious what the intent of this Idris function is: `f : Vect n (Vect m a) -> Vect m (Vect n a)` (where `Vect` is the type of lists of a given length).
For example, it's quite obvious what the intent of this Idris function is: `f : Vect n (Vect m a) -> Vect m (Vect n a)` (where `Vect` is the type of lists of a given length).