Implict parameters and monomorphism

[Marcin 'Qrczak' Kowalczyk]

4 May 2001 18:50:30 GMT, Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> pisze:

> f :: (IArray a e, Ix i) => a i e -> a i e
> f arr = runST (do
>     marr <- thaw arr
>     do some stateful operations on marr
>     freeze marr)

Actually using pattern type signatures alone is almost enough here:

f:: (IArray a e, Ix i) => a i e -> a i e
f arr = runST (do
    (marr :: STArray s i e) <- thaw arr
    do some stateful operations on marr
    freeze marr)

except that ghc has a small bug: pattern type signatures don't
introduce type variables in the 'do' notation, as they do in lambda
arguments. Rewriting it to use '>>=' and lambdas instead of 'do' helps:

f:: (IArray a e, Ix i) => a i e -> a i e
f arr = runST (
    thaw arr >>= \(marr :: STArray s i e) ->
    do some stateful operations on marr >>
    freeze marr)

But doesn't solve completely. There is a strange error message "Could
not deduce `MArray (STArray s1) e (ST s)' from the context (IArray a e,
Ix i)" with two suggested resolutions, both bogus.

The problem is with 's': it's not bound by lambda but eaten by runST.
I have to move the argument of runST to a separate function, to bind
's' in its result type signature, to be able to use it in the pattern
type signature of marr.

This situation can be improved. There was a discussion three months
ago about making pattern and result type signatures one-way matching.

Currently if a part of the type of an argument is not a type
variable bound at the given place, I can't write a type variable in
the appropriate pattern type signature, but must spell the inferred
type. Except that its context is not written. For example changing
'e' in the type of f above into 'Int' makes the type signature on
marr illegal: I must write 'STArray s i Int' too.

This is especially tricky in the presence of fundeps, because whether
a type is fully determined is not necessarily obvious if it's deduced
from fundeps. Ghc requires the programmer to manually follow fundeps
to infer the same amount that ghc knows, instead of specifying just
the part of the type I am interested in.

Another bad case is above. The problematic type is not bound by the
given lambda, it's not a constant, and it's not bound by a pattern
outside either. It's a free type variable of the argument of runST,
eaten by runST. There is no way to write it except by moving the body
of runST to a separate function with a result type signature.

I would like to make pattern and result type signatures one-way
matching, like in OCaml: a type variable just gives a name to the given
part of the type, without constraining it any way - especially without
"negative constraining", i.e. without yielding an error if it will
be known more than that it's a possibly constrained type variable...

SimonPJ sais he agreed and asked Hugs people what they think, and
they didn't reply. This reminds me the 'with' story :-(

This change, together with fixing pattern type signatures in 'do',
would make the function at the top legal.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK