Incoherence

[Koen Claessen]

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?)

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.)

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.

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.