Dependently-typed programming

Dependently-typed programming refers to type-level programming where prior data types determine the types of subsequent values.

By doing type-checking computations, the dependently-typed programming style allows for more nuanced type definitions. For instance, instead of defining a type for "list of numbers", we might go further with the dependently-typed "list of numbers of size n" or "list of distinct strings".

For example, it is easy to implement sprintf in an untyped way, but this function is notoriously difficult to implement in a type-safe language because the return type depends on the value of the format string:

  sprintf "%s"  :: String -> String
  sprintf "%d"  :: Int -> String

To do this in Haskell, we require dependently-typed programming. Let's explore a simplified example (refer to Fun with Types, Kiselyov et al, for more information). First, we create an embedded language for format strings:

  data L      -- literals e.g. "hello"
  data V val...