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.