10 Mar
2013
10 Mar
'13
4:48 p.m.
On Mon, Mar 11, 2013 at 1:33 AM, Kim-Ee Yeoh
class MyTheory a where someKindOfChoice :: a -> [a] -> [a]
Whoops, that should be [a] -> [a], or perhaps more usefully [a] -> a. In a way, such a function constructively /proves/ that the type is infinite. Of course, it has to satisfy a bunch of conditions. You can sort of see how going down this path leads naturally to Coq and Agda. -- Kim-Ee