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
Stringat runtime but got
|Value-Level Programming||Writing source code that gets executed during runtime||Node / Browser|
|Type-Level Programming||Writing source code that gets executed during compile-time||Type Checker / Type Class Constraint Solver^|
^ First heard of this from @natefaubion in the PureScript chatroom.
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,
Thus, when we write...
value1 :: MyType value1 = Value1
... we could also write it with more type information:
value1 :: MyType value1 = (Value1 :: MyType)
(Value1 :: MyType) means
Value1 is a value of the
MyType type (or
Value1 is a member of the
Functions can be either pure or impure. Pure functions have 3 properties, but the third (marked with
*) is expanded to show its full weight:
|Pure||Pure Example||Impure||Impure Example|
|Given an input, will it always return some output?||Always|
|Given the same input, will it always return the same output?||Always |
|*Does it interact with the real world?||Never||Sometimes|
|*Does it acces or modify program state||Never|
Original list is copied but never modified
|*Does it throw exceptions?||Never||Sometimes|
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"
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.
Previously, we said:
Kinds = "How many more types do I need defined before I have a 'concrete' type?"
And using the table from earlier...
|Box a||Type -> Type||Higher-Kinded Type (by 1)|
One type needs to be defined before the type can be instantiated
|(a -> b)|
Function a b
|Type -> Type -> Type||Higher-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:
|Kind||A "Type" for type-level programming|
|Type||The "kind" (i.e. type-level type) that indicates a value-level type for value-level programming|
Sometimes, pictures say a lot more than words:
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.
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
|TYPE-LEVEL EXPRESSION||Inferred kind|
Type-Level programming has 2-3 stages:
- 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
- (optional) Modify that value during compile-time
- Constrain types, so that an impossible state/code fails with a compiler error
- Reflection - convert a type-level value stored in the
Proxytype into a value-level value