Haskell - polymorphism and values depending on types
From reading the Wikipedia entry for a lambda cube and this topic , when applied to Haskell, I understand that
- a family of terms indexed by terms - typical value-to-value function
- a family of terms indexed by type - ??
- type-indexed family of types - parametric polymorphism in type constructors, type families
- a family of types indexed by terms - pi types (in which you forge homogeneous types in Haskell), sigma types, etc.
Please correct me if I am wrong with the examples listed above. Quoting from this Wikipedia article:
- Conditions depending on types or polymorphism. System F, in other words, the second-order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.
I don't know how Haskell fits into this (2) from above. Haskell has a strong distinction between terms and types and erases the type, so you don't have reflection elements in OOP like typeof(a)
or b.GetType()
, and then proceed to return some value based on the type information at runtime.
So the only thing I can think of in Haskell referring to (2) is perhaps
- Return type polymorphism in text
mempty
cData.Monoid
where value depends on instance type - Data families where you take types on LHS and have value constructors on RHS
Will it be right? Although I feel like I haven't made all the connections ...
Can we say that ad-hoc polymorphism satisfies (2) and parametric polymorphism satisfies (3)? But then how does ad-hoc vs parametrically relate to the difference in RHS types with data families?
Last, how would I sum type values like
-
Nothing :: forall a. Maybe a
-
Right 3 :: forall a. Num b => Either a b
when they lack the context of the type that fits into this picture? I'm assuming this is example (2)?
source to share
Conditions indexed by type
In a 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 created by explicitly applying them to types:
boolId : Bool -> Bool boolId = id Bool
In Haskell, a custom language has no explicit application of type and abstraction, since type inference can fill in the details in most (but not all) cases. In contrast, GHC Core, an intermediate language for GHC Haskell, is very similar to the F system and has a generic application.
Erasing styles is orthogonal, whether terms can be indexed by type. This is so that in Haskell, types can be removed from the runtime, but we could imagine other languages that do not have uniformly distributed runtime objects, and therefore would need to preserve types (or size information).
Types indexed by type
In the sense of a lambda cube, this means having functions from types and type constructors to types and types of constructors.
Haskell doesn't have a similar feature. The type of family is getting closer, but they are weaker and stronger.
Generic Classes and Lambda Cube
Generic classes are strange beasts that are not modeled in a lambda cube. In Haskell, they get distracted by functions and word translation, so they don't even appear in GHC Core. They can be thought of as some kind of preprocessing of programs that rely on self-tuning uniqueness of instances to fill in the details deterministically.
source to share