An Overview of Terms and Concepts

Comparison

In programming, there are usually two terms we use to describe "when" a problem/bug/error can occur:

  • Compile-time: Turns source code into machine code. Compiler errors occur due to types not aligning.
  • Runtime: Executes machine code. Runtime errors occur due to values of types not working as expected/verified by the compiler (e.g. you expected a String at runtime but got null).

Definition

TermDefinition"Runtime"
Value-Level ProgrammingWriting source code that gets executed during runtimeNode / Browser
Type-Level ProgrammingWriting source code that gets executed during compile-timeType Checker / Type Class Constraint Solver^

^ First heard of this from @natefaubion in the PureScript chatroom.

What Are Types and Functions?

Types Reexamined

When we define a type like so...

data MyType
  = Value1
  | Value2

... we are saying there is a set or domain called MyType that has two members, Value1 and Value2. Thus, when we write...

value1 :: MyType
value1 = Value1

... we could also write it with more type information:

value1 :: MyType
value1 = (Value1 :: MyType)

The syntax (Value1 :: MyType) means Value1 is a value of the MyType type (or Value1 is a member of the MyType set/domain)

Functions Reexamined

Functions can be either pure or impure. Pure functions have 3 properties, but the third (marked with *) is expanded to show its full weight:

PurePure ExampleImpureImpure Example
Given an input, will it always return some output?Always
(Total Functions)
n + mSometimes
(Partial Functions)
4 / 0 == undefined
Given the same input, will it always return the same output?Always
(Deterministic Functions)
1 + 1 always equals 2Sometimes
(Non-Deterministic Functions)
random.nextInt()
*Does it interact with the real world?NeverSometimesfile.getText()
*Does it acces or modify program stateNevernewList = oldList.removeElemAt(0)
Original list is copied but never modified
Sometimesx++
variable x is incremented by one.
*Does it throw exceptions?NeverSometimesfunction (e) { throw Exception("error") }

Pure functions can better be explained as mapping some input to some output. The simplest example is pattern matching:

data Fruit = Apple | Orange

stringify :: Fruit -> String
stringify Apple = "Apple"
stringify Orange = "Orange"

The function, stringify, doesn't "do" anything: it doesn't modify its arguments, nor does it really "use" its arguments in some manner. Rather, it merely defines what to output when given some input.

In this way, functions merely specify how to map values of some type (e.g. Fruit) to values of another type (e.g. String). This idea is the heart of Category Theory. Thus, types and functions go hand-in-hand.

Kinds Redefined

Previously, we said:

Kinds = "How many more types do I need defined before I have a 'concrete' type?"

And using the table from earlier...

ExampleKindMeaning
StringTypeConcrete value
IntTypeConcrete value
Box aType -> TypeHigher-Kinded Type (by 1)
One type needs to be defined before the type can be instantiated
(a -> b)
Function a b
Type -> Type -> TypeHigher-Kinded Type (by 2)
Two types need to be defined before the type can be instantiated

This definition sufficed when we were learning only value-level programming. In reality, it's more like this:

NameMeaning
KindA "Type" for type-level programming
TypeThe "kind" (i.e. type-level type) that indicates a value-level type for value-level programming

Sometimes, pictures say a lot more than words: comparing-kinds-with-types

We can now modify the definition to account for this new understanding:

Kinds = "How many more type-level types do I need defined before I have a 'concrete' type-level type? Also, the kind, Type, is a type-level type whose 'values'/'members' are value-level types.

Summary of Inferred Kinds

Returning to a table we showed previously, we'll add the header that we removed (all caps) when we first displayed the table and include Record/Row.

TYPE-LEVEL EXPRESSIONInferred kind
UnitType
Array BooleanType
ArrayType -> Type
Either Int StringType
Either IntType -> Type
EitherType -> Type -> Type
Record (foo :: Int)Type
RecordRow Type -> Type
(foo :: Int)Row Type
......

Type-Level Programming Flow

Type-Level programming has 2-3 stages:

  • Creation
    • Define a type-level value by declaring a literal one
    • Reification - convert a value-level (i.e. runtime value) value into a type-level value via a Proxy type
  • (optional) Modify that value during compile-time
  • Terminal
    • Constrain types, so that an impossible state/code fails with a compiler error
    • Reflection - convert a type-level value stored in the Proxy type into a value-level value

Related Papers