Difference between revisions of "HaskellImplementorsWorkshop/2012/Diatchki"
(New page: =Implementing Type-Level Literals in GHC= ''Iavor Diatchki'' Type-level literals, such as natural numbers and string symbols, are useful for implementing safer Haskell libraries. For exa...) |
(Added Category:Community) |
||
| Line 15: | Line 15: | ||
will give an update of the current state of the constraint solver, |
will give an update of the current state of the constraint solver, |
||
which adds support for type-level computation involving numbers. |
which adds support for type-level computation involving numbers. |
||
| + | |||
| + | |||
| + | [[Category:Community]] |
||
Latest revision as of 13:44, 17 December 2012
Implementing Type-Level Literals in GHC
Iavor Diatchki
Type-level literals, such as natural numbers and string symbols, are useful for implementing safer Haskell libraries. For example, natural numbers in the types may be used to keep track of the sizes of various data structures (e.g., arrays or bit-vectors), while string symbols can be used as an infinite source of labels (e.g., to refer to statically known resources). In this talk, I will present some of the details of the implementation of type-level literals in GHC. In particular, I will discuss the overall design, the supporting libraries for programming with type-level literals, and demonstrate some techniques for writing programs with these libraries. Finally, I will give an update of the current state of the constraint solver, which adds support for type-level computation involving numbers.