A very good point. But that just makes a design that could include
Id even more intriguing. :)
-- Lennart
On Mar 22, 2007, at 01:21 , [EMAIL PROTECTED] wrote:
Lennart Augustsson wrote:
Ganesh and I were discussing today what would happen if one adds Id
as a primitive type constructor. How much did you have to change the
type checker? Presumably if you need to unify 'm a' with 'a' you now
have to set m=Id.
I wonder if this proposal is a good idea.
Let us consider the following near-Haskell98 code
class C a
instance C (m a)
instance C Int
(usually there will be constraints on m. We shall see a useful
example of
this in a moment). This code typechecks under slight and common
relaxation of the rules on the form of instance head. That example
will probably typecheck in Haskell'.
Under the proposal that Id t === t, typechecking
of this code will require overlapping instances, which quite
unlikely to
make it into Haskell' and is a quite significant and controversial
extension.
Speaking of overlapping instances, let's generalize the example to
class C a
instance C (m a)
instance C a
It does typecheck in current Haskell. Under the Id proposal, this
example will NOT typecheck, ever. This is because the two instances
become exact duplicates. Indeed, every type that matches "a" will
match "m a" (with m = Id) and vice versa. The two instances match the
same class of types (that is, all of the types).
Let us come back to our simple example and make it practical.
class C a where incr :: a -> a
instance (C a, Functor m) => C (m a) where incr = fmap incr
instance C Int where incr = succ
test = incr (Just [[[1::Int]]])
the example increments integers deeply embedded in some functorial
data structures. The operations of this kind are requested from time
to time on Haskell-Cafe. This code compiles and works (no overlapping
or undecidable instances are required). Under the Id t === t
proposal, this example will diverge (perhaps, it will diverge even in
the compiler). The reason is that the base case cannot be reached; the
type Int can always be considered as Id Int and so the first instance
will apply again.
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
