On Sat, Mar 9, 2013 at 7:25 AM, Heinrich Ody
I'm given a type 'a' (lets assume the type is infinite) and a set finite 'xs'. Now I want to create a new value of type 'a' that does not occur in 'xs' and return a set 'ys' that consists of 'xs' and also contains the new value.
Is this a wish to explore some variant of a choice axiom in Haskell? I'm afraid there's no such thing. Being given a type is not the same as being given a set, notwithstanding the modelling of list comprehension after set comprehension. Much of this becomes totally obvious when you look at System F, a variant of which forms the lower-level core language of GHC. And the way to approach System F, which is forbidding at first glance, is that it's just Haskell except that all the type functions and applications are made explicit. p.s. You can actually roll your own set theory using type classes: class MyTheory a where someKindOfChoice :: a -> [a] -> [a] -- Kim-Ee