[Haskell-cafe] Typing with co/contra-variance.
Ben.Lippmeier at anu.edu.au
Thu Apr 3 05:58:33 EDT 2008
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 :: Int -> Bool
= 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.
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?
2) This seems simpler than real intersection types, which I know are
problematic. If I only want 'Top' and not a real object system like in
Scala or Java, then can I just add this to a HM/unification style
inference algorithm and expect it to work? I'm thinking the unifier only
needs to know the variance of the types it's unifying to decide whether
to throw an error or return Top - or will there be problems with higher
order functions etc?
I had a read through the subtyping chapter in "Types and Programming
Languages" by Pierce - it gives the typing rules but don't mention
inference or implementations.
Scala seems to have this
(http://www.scala-lang.org/intro/variances.html) but as I understand it,
their system doesn't support full type inference without user supplied
BTW: searching for 'the any type' in Google helps even less than you
might expect :)
More information about the Haskell-Cafe