3 ms·
Well, as you go to the next steps you can use proof search techniques to do exactly that: write your types and your programs write themselves as the "only possi
by tel 13y ago
Well, as you go to the next steps you can use proof search techniques to do exactly that: write your types and your programs write themselves as the "only possible implementation".
This is already possible sometimes in Haskell so long as we restrict ourselves from pathological values like exceptions and non-termination. In fact, the first place this phrase shows up is Russel O'Connor talking about highly polymorphic lens code.
http://r6.ca/blog/20120708T122219Z.html http://r6.ca/blog/20120708T122219Z.html
This kind of type limitation of possible implementations is called parametricity and is difficult to encounter even in most typed languages as it requires purity.
- dllthomas 13y agoThe first place which phrase shows up?
- tel 13y agoMm, I think I went too far there. I was thinking "confession of a Haskell hacker" but got that conflated with "if it types, it's right".
- laureny 13y 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 13y 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 13y ago> law-abiding implementations Are you referring to category laws?