Haskell - polymorphism and values depending on types

3
votes

From reading Wikipedia entry for lambda cube and this thread, when apply to Haskell, my understanding is that

  1. family of terms indexed by terms - typical function from value to value
  2. family of terms indexed by types - ??
  3. family of types indexed by types - parametric polymorphism in type constructors, type families
  4. family of types indexed by terms - pi types (in which you fake with singleton types in Haskell), sigma types, etc...

Please correct me if I got the examples listed above wrong. Quoting from that Wikipedia article:

  • Terms depending on types, or polymorphism. System F, aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.

I do not know how Haskell fits into this (2) from above. Haskell has a strong distinction between terms and types, and type erasure, so you do not have reflection stuff in OOP such as typeof(a) or b.GetType(), and then proceed to return some value based on type information at run time.

So the only thing I can think of in Haskell relating to (2) are maybe

  • Return type polymorphism in say mempty in Data.Monoid, where the value depends on the instance type
  • Data families where you take in types on the LHS and have value constructors on the RHS

Would that be correct? Though I feel like I didn't make all the connections...

Would it be correct to say ad-hoc polymorphism satisfies (2) while parametric polymorphism satisfies (3)? But then how does ad-hoc vs parametric relates to difference in RHS of type vs data families?

One last thing, how would sum type values such as

when they lack type context fit into this picture? My guess would be that this is an example of (2)?

1
haskellpolymorphismlambda-calculustype-families

1 Answers

4
votes

Terms indexed by types

In the lambda cube this is parametric polymorphism.

In System F, polymorphic terms look like functions that take types as arguments and return terms.

id : ∀ a. a -> a
id = Λa . λx : a . x    -- Λ binds type args, λ binds term args

They can be instantiated by explicitly applying them to types:

boolId : Bool -> Bool
boolId = id Bool

In Haskell, the user-facing language doesn't have explicit type application and abstraction, because type inference can fill in the details in most (but not all) cases. In contrast, GHC Core, the intermediate language for GHC Haskell, closely resembles System F and does have type application.

Type erasure is orthogonal to whether we can index terms by types. It happens so that in Haskell types can be erased from runtime, but we could imagine other languages that don't have uniformly sized runtime objects, and thus they'd need to keep types (or size information) around.

Types indexed by types

In the lambda cube sense this means having functions from types and type constructors to types and type constructors.

Haskell doesn't quite have an analogous feature. Type families come closest, but they are both weaker and stronger.

Type classes and the lambda cube

Type classes are strange beasts that aren't modeled in the lambda cube. In Haskell they desugar into functions and dictionary passing, so they don't even show up in GHC Core. They can be seen as some sort of preprocessing on programs that relies on the self-imposed uniqueness of instances to deterministically fill in details.