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:

  1. A relationship that can define multiple type-level functions.
  2. 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 TypeValue-Level Value(s)Kind Name
(Corresponding Type‑Level Type)
Kind Values
OrderingLT GT EQOrderingLT GT EQ
String"literal string"Symbol"literal symbol"
(closest idea)
Record (keyN :: VTN, ...)row kinds(keyN :: Kind, ...)
List ( keyN :: VTN, ... )
(analogy; not real type)

Cons a (ListR a)

Cons :: 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.

^^ 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