[Haskell-beginners] Create new value for given type

[Kim-Ee Yeoh]

On Sat, Mar 9, 2013 at 7:25 AM, Heinrich Ody <heinrich.ody at gmail.com> wrote:
> 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