the types sing
joeyh at
Been working on and off all week on some code and a lot of types to go with the code. I just deleted all the code, replacing it with the single word sing.
The types, you see, grew good enough that the code was not necessary to explain to the compiler what needs to be done. Dependently typed programming with singleton types. A milestone for me.
Claes Wallin (韋嘉誠) likes this.
Claes Wallin (韋嘉誠) shared this.
For example, 2 lines of comments:
-- | Changes the target of a property. -- -- This can only tighten the target list to contain fewer targets.
4 lines of type information:
target
:: (combined ~ Intersect old new, CheckCombineTargets old new ~ CanCombineTargets)
=> Targeting new
-> Property (WithTypes old)
-> Property (WithTypes combined)
1 line of trivial implementation:
target new (Property old a) = Property sing a