Re:Notes on Idris (2017)
by alexashka on Thursday June 07, 2018 @02:59PM
(#17259017)
The removeLast() function signature would be UntypedCollection (S n) -> UntypedCollection n
(S n) stands for successor of n. (Think of (S n) as n+1)
Given this, you can't call removeLast() on an UntypedCollection Z (empty collection) because the types wouldn't match.
So it's not by magic - the compiler knows the number of elements in the collection, because that value is part of the type. That's the entire point of dependent types - you get to have any value as part of a type.
The part that becomes tiresome very quickly - is convincing the type checker that what you want is valid. You have to provide proofs for the most trivial things (2+1 = 1+2) and the way it is currently achieved, is not programmer friendly.
(S n) stands for successor of n. (Think of (S n) as n+1)
Given this, you can't call removeLast() on an UntypedCollection Z (empty collection) because the types wouldn't match.
So it's not by magic - the compiler knows the number of elements in the collection, because that value is part of the type. That's the entire point of dependent types - you get to have any value as part of a type.
The part that becomes tiresome very quickly - is convincing the type checker that what you want is valid. You have to provide proofs for the most trivial things (2+1 = 1+2) and the way it is currently achieved, is not programmer friendly.