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

Ben Lippmeier Ben.Lippmeier at anu.edu.au
Thu Apr 3 05:58:33 EDT 2008

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"

  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.

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 :)

Thanks, Ben.

More information about the Haskell-Cafe mailing list