This is the second part in my two-part series on Leibniz equality in Haskell. See here for part 1. Part 2 will build on ideas and concepts from part 1, so if you haven’t read part 1 yet, go do so!
Continue reading »When using types, one often asks the question: when are two types
the same? There are many different ways to encode the sameness of two types.
In GHC, one of the most common ways is through
this data type,
defined in Data.Type.Equality:
In GHC, many language features available at the term level can be straightforwardly promoted to the type level. For example, the following term-level function:
Continue reading »If you write enough Haskell programs, it’s quite likely that you’ll want to define a function whose body mentions a type variable that is bound by its type signature. Here is a very simple example:
Continue reading »GHC 8.10.1 is slated to be released
soon,
and among the improvements that it offers is the
new StandaloneKindSignatures language extension. Standalone kind
signatures (or “SAKS” for short) are like type signatures, except that they
describe type-level declarations instead of term-level values. Here is one
example of a standalone kind signature that describes the kind of a type
synonym:
