[Haskell-cafe] Typing with co/contra-variance.

[Luke Palmer]

On Thu, Apr 3, 2008 at 9:58 AM, Ben Lippmeier <Ben.Lippmeier at anu.edu.au> wrote:
> 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