On Thu, Apr 3, 2008 at 9:58 AM, Ben Lippmeier
Hi all, I have some quick questions for the type theory people:
If I write an expression: (if .. then 23 else "Erk")
In Haskell this would be an error, but perhaps I can assign it the type 'Top' (or 'Any') and then use reflection ala Data.Dynamic to inspect the type of this object at runtime and cast it back to something useful...
But if I write:
isEven "Erk"
where isEven :: Int -> Bool isEven i = case i of 1 -> False 2 -> True ...
Then this would be a genuine type error, because the case-expression demands an actual Int at runtime.
Questions: 1) Could I perhaps wave my arms around and say something about the Int in the type of isEven being in a contra-variant position? Is this what is actually happening?, and can someone point me to a good paper?
This is related to "gradual typing". I don't know how much work has been done into inference for gradual typing, but I'll bet you could hack on the HM algorithm a little and get something usable. Here's a relevant paper: http://www.cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual.pdf Enjoy. Luke