Incoherence

[John Hughes]

	John Hughes wrote:

	 | `x := []' wouldn't be problematic, just monomorphic.
	 | That is, x must be used consistently as a list of a
	 | particular type.

	Just to check if I understand you correctly. In your
	proposal, does the following thing share `x'?

	  let x = fac 100 in x + x

	(My understanding is that, in order to do this in your
	proposal, we have to say:

	  let x := fac 100 in x + x

	Correct?)

Correct.

	Does this also mean that it becomes impossible to share
	polymorphic values? I.e. the following contrived example
	will not behave as usual:

	  wrong :: Either String a
	  wrong = Left (show (fac 100))  -- not shared?

	  example1 :: Either String Int
	  example1 :=
	    do wrong
	       return 1

	  example2 :: Either String Char
	  example2 :=
	    do wrong
	       return 'a'

	(With the usual Either monad instance.)

Also true.

	Of course, in this case, there is a perfect remedy, just
	lifting out `show (fac 100', which is a monomorphic
	expression.

	However, this is not always possible, we might have a
	datatype like this:

	  data PolyMonoList a
	    = Poly Int (Foo a)
	    | Mono a   (Foo a)
	    | Nil

	We can construct rather large polymorphic values, which have
	to be converted in linear time to the same value of a
	different type.

Yup.

	I guess we already have the problem of not being able to
	share monomorphic values polymorphically. In fact, the
	Either monad instance is a good example:

	  instance Monad (Either e) where
	    return = Right

	    Left x  >>= k = Left x
	    Right a >>= k = k a

	In the definition of `>>=', it is impossible to share `Left
	x'.

	/Koen.

All true, but I doubt whether any of this is a big deal. MLers already live
with their "value restriction", which has similar penalties, so there is a
precedent.

John