Type-Level Primitives
In addition to Custom Type Errors, the Prim module has sub modules that are not imported by default. Within these modules, Prim defines a few more things for type-level programming. These type classes' instances are derived by the compiler
Types of Relationships
As explained in the Syntax folder, we use logic programming and unification to compute type-level expressions. To define type-level functions, we define a relationship and the various ways (functional dependencies) that the types can unify. However, there are actually two types of relationships in type-level programming:
- A relationship that can define multiple type-level functions.
- A relationship that can assert that something is true.
The first one is easy to understand and is used frequently. However, we have never mentioned assertion relationships. For some examples, see these type classes:
In my current understanding, I'd guess that these likely do not appear that often in type-level code, but they may be critical for some use cases.
Type-Level Types, Values, and Proxies
In the below table, "ValueTypeN" was abbreviated to VTN
| Value-Level Type | Value-Level Value(s) | Kind Name (Corresponding Type‑Level Type) | Kind Values |
|---|---|---|---|
| Ordering | LT GT EQ | Ordering | LT GT EQ |
| String | "literal string" | Symbol | "literal symbol" |
| Int | 1(-1) | Int | 1(-1) |
| Record (closest idea) | Record (keyN :: VTN, ...) | row kinds | (keyN :: Kind, ...) |
| Boolean | true/false | Boolean | True/False |
| List ( keyN :: VTN, ... ) (analogy; not real type) | NilCons a (ListR a) | RowList | NilCons :: Symbol -> Type -> RowList |
Type-Level Modules
Rather than explaining things, read through the source code of these modules and you should be able to get a good intuition for how this stuff works. For additional examples, see the Ecosystem folder and check out some of the data structures (e.g. Array, Matrix) that have been augmented with type-level programming.
| Kind | Modules |
|---|---|
| Boolean | Prim.Boolean |
| Ordering | Prim.Ordering |
| Symbol | Prim.Symbol Type.Data.Symbol |
| Int | Prim.Int |
| Row | Prim.Row Type.Row Type.Row.Homoegeneous Record Heterogenous^^ |
| RowList | Prim.RowList |
| Higher-Order Functions | Type.Eval |
| N/A | Type.IsEqual Type.Proxy |
^^ The purescript-heterogenous library is mind-blowing and is exlained by its author in the following video. This video is potentially difficult-to-understand but will make more sense as one gets used to more FP concepts. Around 14 minutes in, Nate gets up and moves elsewhere. So, skip to 16:37 when this occurs to avoid wasting time:
PS Unscripted - Heterogenous