5 ms·
> write your types and your programs write themselves as the "only possible implementation". But there are only very few type signatures for which this is true
by laureny 12y ago
> write your types and your programs write themselves as the "only possible implementation".
But there are only very few type signatures for which this is true, even if you stick to totality.
- tel 12y agoIn practice types often winnow the possible implementations to be a relatively small set. This effect is improved if you also include notions of law-abiding implementations as Haskellers often do. At the end of the day, it's true that implementations (don't yet) write themselves, but, more realistically, that the constraints of type and theory drive you naturally to the correct solutions even if you never once figure out the "operational" aspect. That occurs quite often.
- ademarre 12y ago> law-abiding implementations Are you referring to category laws?