OpenUniverse.idr

module OpenUniverse

data IntSpec : Type where
  INT : IntSpec

data StringSpec : Type where
  STRING : StringSpec

interface Interpolation (a : Type) where
  total
  interpCode : a -> Type

  total
  stringify : {b : a} -> interpCode b -> String

||| We support printing integers.
Interpolation IntSpec where
  interpCode INT = Int
  stringify {b=INT} = show

||| We support printing strings.
Interpolation StringSpec where
  interpCode STRING = String
  stringify {b=STRING} = id

||| A format specifier is a list with two cases in each cons cell. Either we
||| want to print out a literal string or we want to interpolate something into
||| the output. Interpolation is handled by the 'Interpolation' interface.
data Format : Type where
  Interpolate : Interpolation a => a -> Format -> Format
  Literal : String -> Format -> Format
  End : Format

||| Boxes an 'Interpolation' constraint for a type.
data InterpBox : Type where
  Box : Interpolation a => a -> InterpBox

||| Converts a format specifier into a list of boxed 'Interpolation'
||| constraints. This list can be consumed by 'interpType'.
formatArgs : Format -> List InterpBox
formatArgs End = []
formatArgs (Literal _ f) = formatArgs f
formatArgs (Interpolate x f) = Box x :: formatArgs f

||| Computes the type of a function that interpolates its arguments according
||| to the given list of interpolation requirements.
interpType : List InterpBox -> Type
interpType [] = String
interpType ((Box x) :: xs) = interpCode x -> interpType xs

||| Computes the body of the interpolation function adhering to the given
||| format.
toFunction : (f : Format) -> String -> interpType (formatArgs f)
toFunction End acc = acc
toFunction (Literal s f) acc = toFunction f (acc ++ s)
toFunction (Interpolate x f) acc = \s => toFunction f (acc ++ stringify {b=x} s)

||| Type-safe printf.
||| Sadly, we don't yet have a parser for format strings.
printf : (f : Format) -> interpType (formatArgs f)
printf f = toFunction f ""

-- Now an example

-- Some syntactic sugar to make writing format specifiers easier.
infixr 3 &
infixr 3 #

(#) : Interpolation a => a -> Format -> Format
(#) = Interpolate

(&) : String -> Format -> Format
(&) = Literal

example1 : String -> Int -> String
example1
  = printf (STRING # " is awesome for at least " & INT # " reasons." & End)

concreteExample1 : "idris is awesome for at least 3 reasons."
                 = example1 "idris" 3
concreteExample1 = Refl

-- And we can extend our printf with new instances.

data CharSpec : Type where
  CHAR : CharSpec

Interpolation CharSpec where
  interpCode CHAR = Char
  stringify {b=CHAR} = show

example2 : Char -> Int -> String
example2 = printf (CHAR # " is the " & INT # "th letter of the alphabet." & End)

concreteExample2 : "'d' is the 4th letter of the alphabet." = example2 'd' 4
concreteExample2 = Refl