On 3/19/07, <b class="gmail_sendername">Lennart Augustsson</b> <<a href="mailto:lennart@augustsson.net" target="_blank" onclick="return top.js.OpenExtLink(window,event,this)">lennart@augustsson.net</a>> wrote:<div><span class="gmail_quote">
</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Ravi,<br><br>Ganesh and I were discussing today what would happen if one adds Id<br>as a primitive type constructor. How much did you have to change the<br>type checker? </blockquote><div><br>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).
<br></div><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Presumably if you need to unify 'm a' with 'a' you now<br>have to set m=Id. Do you know if you can run into higher order
<br>unification problems? My gut feeling is that with just Id, you<br>probably don't, but I would not bet on it.</blockquote><div><br>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.
<br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Having Id would be cool. If we make an instance 'Monad Id' it's now
<br>possible to get rid of map and always use mapM instead. Similarly<br>with other monadic functions.<br>Did you do that in the Bluespec compiler?</blockquote><div><br>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.
<br><br>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):
<br> - 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.
<br> - make sure not to replace m with Id, if m is a lexically-bound type variable<br> - make sure to expand type synonyms before attempting this sort of unification<br><br>After that I could typecheck simple things like the following (using an inferred identity monad):
<br><br>x :: Integer<br>x = return 5<br><br>y :: List Integer<br>y = mapM (const 5) (cons 1 (cons 2 nil))<br><br>However, I did run into the problems Iavor and Simon mentioned. For example, the following program did not typecheck:
<br><br>z :: Bool -> Maybe (Integer)<br>z p1 = let f a0 b0 =<br> let a = return a0<br> b = return b0<br> in if p1 then a else b<br> in f 5 (Just 6)<br><br>
However, the same could *would* typecheck if I added the following type annotations:<br><br>z :: Bool -> Maybe (Integer)<br>
z p1 = let f a0 b0 =<br>
let a = return (a0 :: Integer)<br> b = return (b0 :: Maybe Integer)<br>
in if p1 then a else b<br>
in f 5 (Just 6)<br>
<br>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.
<br> <br> - Ravi<br></div></div>