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
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.
In the below table, "ValueTypeN" was abbreviated to VTN
|Value-Level Type||Value-Level Value(s)||Kind Name|
(Corresponding Type‑Level Type)
|List ( keyN :: VTN, ... )|
(analogy; not real type)
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.
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