This folder assumes you have read through and are familiar with
Type Level Syntax. If you aren't, go and read through that first.
Taken from this SO answer (last paragraph), type-level programming can be used to:
restrict certain behavior at the value-level, manage resource finalization, or store more information about data-structures.
Let's explain a problem that highlights the third point: storing more information about data-structures. Below is one problem that occurs at the runtime that can be fixed with type-level programming.
Array is a very fast data structure, but it's problematic because we never know its exact size at compile-time. In other words, we don't get a compiler error if we reference an invalid spot in the array, and we won't know about the bug until it occurs when running the program. In short, this kind of function will always be a partial function.
Here's an example in code. If the array is empty or has fewer than
n - 1 elements, the function can only throw an error when we try to reference a non-existent element at index
n. If the array has
n - 1 or more elements, it can return that element.
elemAtIndex :: forall a. Partial => Int -> Array a -> a elemAtIndex idx  = Partial.crash "cannot get " <> show idx <> "th element of an empty array" elemAtIndex index fullArray = unsafePartial $ unsafeIndex fullArray index
What if we could modify the type of
Array, so that it included the size of that array at compile-time? Then, the type-checker could ensure that the "elemAtIndex" function described above only receives correct arguments (i.e. specific types) that make the function "total," meaning the function will always return a valid output and never throw an error. If it receives an invalid argument, it results in a compiler error and we can fix the bug before shipping the code to customers.
-- This entire block of code is pseduo syntax and does not actually work! -- Use it only to get the idea and don't hold onto any of the syntax used here. elemAtIndex :: forall a n. HasElemAtIndex n => n -> IndexedArray n a elemAtIndex index array = -- implementation elemAtIndex 3 (IndexedArray 3 [0, 1, 2, 3]) -- 3 elemAtIndex 3 (IndexedArray 3 [0, 1]) -- compiler error! elemAtIndex 0 (IndexedArray Empty ) -- compiler error!
This is exactly what the library Vec does.
- When using type-level programming, the compiler has to do more work. Thus, it will increase the time it takes to compile your program.
- Creating a type-level value for a kind can get really tedious and boilerplatey. Either reuse ones that exist in libraries or publish your own library for the benefit of the entire community.
Consider purchasing the
Thinking with Types book mentioned in
ROOT_FOLDER/Syntax/Type-Level Programming Syntax/ReadMe.md
spago run -m TLP.SymbolExample spago run -m TLP.IntegerExample spago run -m TLP.RowExample