3
$\begingroup$

Lets say I have two type expressions: 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.

$\endgroup$
  • 2
    $\begingroup$ I'd write "$X$ is more general than $Y$". Type inference usually produces the "most general type". $\endgroup$ – chi May 21 '18 at 16:07
  • $\begingroup$ @chi thanks for pointing that out - and in many places it makes a lot of sense for me to do that. It's got a bit more information in it than simply, saying 'X contains Y', which is a good thing. $\endgroup$ – Liam M May 22 '18 at 6:09
6
$\begingroup$

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 Maybe a in Haskell, intuitively corresponds to the intersection over every type $T$ of the 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}$.

$\endgroup$
  • $\begingroup$ Great answer, thank you for your help. I think I should try and work more in terms of 'instantiation', rather than in the set notation wherever possible, and in occurences where I use the language of sets aim to clarify the underlying mechanics of what I'm doing and seek out more correct language. Anyway - thanks! $\endgroup$ – Liam M May 22 '18 at 6:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.