type aliases and Id

[Ravi Nanavati]

On 3/19/07, Lennart Augustsson <lennart at augustsson.net> wrote:
>
> Ravi,
>
> 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?


All I did is add an expansion rule for my Id constructor to the place where
the SizeOf pseudo-constructor was expanded. This basically means that if the
typechecker sees Id applied so something, it is simplified out (as part of
type-normalization / synonym expansion).

Presumably if you need to unify 'm a' with 'a' you now
> have to set m=Id.  Do you know if you can run into higher order
> unification problems?  My gut feeling is that with just Id, you
> probably don't, but I would not bet on it.


I didn't change the unification rules, so 'm a', would NOT unify with 'a'
with m=Id. That was mainly because I didn't need that unification rule to
handle the case where I used the Id constructor.

Having Id would be cool.  If we make an instance 'Monad Id' it's now
> possible to get rid of map and always use mapM instead.  Similarly
> with other monadic functions.
> Did you do that in the Bluespec compiler?


I did experiment with Monad Id while trying to sort something else out, and
it seemed to work (the instance typechecked as well as some code that
depended on that instance), but I didn't push it very hard.

Beyond that, in response to your note, I tried to see what would happen if I
added a unification rule for 'm a' with 'a', with m=Id. There turned out to
be three important details (to keep existing Bluespec code working):
 - make sure to choose to unify 'm a' with a separate type variable 'b'
directly, in preference to setting m=Id and unifying a with b. Upon
reflection, that seemed reasonable because it didn't prevent setting m=Id
later, in response to additional information.
 - make sure not to replace m with Id, if m is a lexically-bound type
variable
 - make sure to expand type synonyms before attempting this sort of
unification

After that I could typecheck simple things like the following (using an
inferred identity monad):

x :: Integer
x = return 5

y :: List Integer
y = mapM (const 5) (cons 1 (cons 2 nil))

However, I did run into the problems Iavor and Simon mentioned. For example,
the following program did not typecheck:

z :: Bool -> Maybe (Integer)
z p1 = let f a0 b0 =
                 let a = return a0
                       b = return b0
                 in if p1 then a else b
            in f 5 (Just 6)

However, the same could *would* typecheck if I added the following type
annotations:

z :: Bool -> Maybe (Integer)
z p1 = let f a0 b0 =
                 let a = return (a0 :: Integer)
                       b = return (b0 :: Maybe Integer)
                 in if p1 then a else b
            in f 5 (Just 6)

So, I'd say the results were intriguing but not terribly satisfying. My
guess is many common uses would work out, but there would be hard-to-explain
corner cases where the typechecker would need guidance or a desired level of
polymorphism couldn't be achieved.

 - Ravi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20070320/d2bd6538/attachment-0001.htm