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

[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?

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 
annotations...

BTW: searching for 'the any type' in Google helps even less than you 
might expect :)

Thanks, Ben.