patternMinor
How should I describe the relationships between type expressions?
Viewed 0 times
thehowexpressionstypebetweendescribeshouldrelationships
Problem
Lets say I have two type expressions:
What language should I use to describe the relationship between these expressions, and type expressions in general? I've been using the language of sets: X describes a subset of Y, X and Y intersect, and so on. Is this generally accepted, or is there a different, widely accepted language for describing the relationships between type expressions?
In the example provided, I would like to express th at expression X describes many possible types, and that includes all of the types described by Y.
Maybe a (X) and Maybe Integer (Y), where Maybe is a type constructor, Integer is a Type and a is a type variable.What language should I use to describe the relationship between these expressions, and type expressions in general? I've been using the language of sets: X describes a subset of Y, X and Y intersect, and so on. Is this generally accepted, or is there a different, widely accepted language for describing the relationships between type expressions?
In the example provided, I would like to express th at expression X describes many possible types, and that includes all of the types described by Y.
Solution
The set-theoretic intuitions can make sense in the semantics, especially in the context of realizability semantics (where types are interpreted as sets of terms). In this case, the polymorphic type $\forall \alpha. \mathrm{Maybe}(\alpha)$, written
elements of $\mathrm{Maybe}(T)$. Or in other words, $⟦\forall \alpha. \mathrm{Maybe}(\alpha)⟧ = \bigcap_T ⟦\mathrm{Maybe}(T)⟧$, where $T$ ranges over the semantic domain (and elements of the semantics are injected into the syntax).
On the other hand, set-theoretic intuition does not really make sense on the side of the type system, because standard set operations are not allowed. For instance, it is not possible to refer to the intersection of two types in the syntax (at least when you are not working with intersection type systems, and I don't think this is the case in Haskell). However, one operation on types that is primitive in all type systems with polymorphism is instantiation. This corresponds to the elimination rule for the universal quantifier (or polymorphism), and it states that if you have a term $t$ of type $\forall \alpha, \mathrm{Maybe}(\alpha)$ then the term $t$ can be seen as an element of type $\mathrm{Maybe}(T)$ for any type $T$, for example $\mathrm{Integer}$.
Maybe a in Haskell, intuitively corresponds to the intersection over every type $T$ of theelements of $\mathrm{Maybe}(T)$. Or in other words, $⟦\forall \alpha. \mathrm{Maybe}(\alpha)⟧ = \bigcap_T ⟦\mathrm{Maybe}(T)⟧$, where $T$ ranges over the semantic domain (and elements of the semantics are injected into the syntax).
On the other hand, set-theoretic intuition does not really make sense on the side of the type system, because standard set operations are not allowed. For instance, it is not possible to refer to the intersection of two types in the syntax (at least when you are not working with intersection type systems, and I don't think this is the case in Haskell). However, one operation on types that is primitive in all type systems with polymorphism is instantiation. This corresponds to the elimination rule for the universal quantifier (or polymorphism), and it states that if you have a term $t$ of type $\forall \alpha, \mathrm{Maybe}(\alpha)$ then the term $t$ can be seen as an element of type $\mathrm{Maybe}(T)$ for any type $T$, for example $\mathrm{Integer}$.
Context
StackExchange Computer Science Q#92139, answer score: 6
Revisions (0)
No revisions yet.