type aliases and Id

[Lennart Augustsson]

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 , oleg at pobox.com 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime