Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Make some progress on part 11 of compiler series

Browse Source
This commit is contained in:
Danila Fedorin 2020-04-04 23:16:01 -07:00
parent b04d82f0b3
commit 569fea74a7
1 changed files with 44 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
content/blog/11_compiler_polymorphic_data_types.md
View File

@ -51,7 +51,7 @@ I hope that the similarities are quite striking. I claim that
`List` is quite similar to a constructor `Cons`, except that it occurs
in a different context: whereas `Cons` is a way to create values,
`List` is a way to create types. Indeed, while we call `Cons` a constructor,
it's typicall to call `List` a __type constructor__.
it's typical to call `List` a __type constructor__.
We know that `Cons` is a function which
assigns to values (like `3` and `Nil`) other values (like `Cons 3 Nil`, or `[3]` for
short). In a similar manner, `List` can be thought of as a function
@ -61,3 +61,46 @@ even claim that it has a type:
{{< latex >}}
\text{List} : \text{Type} \rightarrow \text{Type}
{{< /latex >}}
{{< sidenote "right" "dependent-types-note" "Unless we get really wacky," >}}
When your type constructors take as input not only other types but also values
such as <code>3</code>, you've ventured into the territory of
<a href="https://en.wikipedia.org/wiki/Dependent_type">dependent types</a>.
This is a significant step up in complexity from what we'll be doing in this
series. If you're interested, check out
<a href="https://www.idris-lang.org/">Idris</a> (if you want to know about dependent types
for functional programming) or <a href="https://coq.inria.fr/">Coq</a> (to see how
propositions and proofs can be encoded in a dependently typed language).
{{< /sidenote >}}
our type constructors will only take zero or more types as input, and produce
a type as output. In this case, writing \\(\\text{Type}\\) becomes quite repetitive,
and we will adopt the convention of writing \\(*\\) instead. The types of such
constructors are called [kinds](https://en.wikipedia.org/wiki/Kind_(type_theory)).
Let's look at a few examples, just to make sure we're on the same page:
* The kind of \\(\\text{Bool}\\) is \\(*\\): it does not accept any
type arguments, and is a type in its own right.
* The kind of \\(\\text{List}\\) is \\(*\\rightarrow *\\): it takes
one argument (the type of the things inside the list), and creates
a type from it.
* If we define a pair as `data Pair a b = { MkPair a b }`, then its
kind is \\(* \\rightarrow * \\rightarrow *\\), because it requires
two parameters.
As one final observation, we note that effectively, all we're doing is
tracking the [arity](https://en.wikipedia.org/wiki/Arity) of the constructor
type.
Let's now enumarate all the possible forms that (mono)types can take in our system:
1. A type can be a placeholder, like \\(a\\), \\(b\\), etc.
2. A type can be a type constructor, applied to
{{< sidenote "right" "zero-more-note" "zero ore more arguments," >}}
It is convenient to treat regular types (like \(\text{Bool}\)) as
type constructors of arity 0 (that is, type constructors with kind \(*\)).
In effect, they take zero arguments and produce types (themselves).
{{< /sidenote >}} such as \\(\\text{List} \; \\text{Int}\\) or \\(\\text{Bool}\\).
3. A function from one type to another, like \\(\\text{List} \\; a \\rightarrow \\text{Int}\\).
Polytypes (type schemes) in our system can be all of the above, but may also include a "forall"
quantifier at the front, generalizing the type (like \\(\\forall a \; . \; \\text{List} \; a \\rightarrow \\text{Int}\\)).