• source ::

Note: code for this book in Idris2can be found here

1. Overview

Type-driven developmentcould be thought of as designing the typesfor a program first, and understanding a program as the interaction of those types.

The concept of types outlined in this chapter sounds very similar to [[file:../20200708122545-category_theory.org][category theory]].

Type-driven development can be used in concurrent programmingby defining an interface that describes the form of messages it will handle and define a protocol describing how the messages will be sent and in what order.

Type-driven development is driven by the following process:

1. Type. Write a type and use it for relevant functions.

2. Define. Write a function that satisfies input and output types using the above type.

3. Refine. Exclude invalid input and output.

Types can be dependent, i.e. is calculated by some other values. Consider a hypothetical append function:

Idrisis a pure functional programminglanguage.

• functional programming:: programs are composed of first class functional constructs, and program execution consists of evaluating those functions

• pure functional programming:: in addition to functional programming, functions do not have side-effectsand all functions are idempotency

Although a pure functional programming language cannot perform side-effects, it can describe them.

• referential transparency:: the property of a function to produce the same output as an input. A key to pure functional programming

In Idris a typethat describes a side-effectis denoted as such, e.g. String vs. IO String.

• total function:: a function that always returns a result

• partial function:: a function that may not return a result given some inputs, i.e. the output is not defined

2. Getting started with Idris

Listing 2.1 code reproduced here for reference:

module Main

average : (str : String) -> Double
average str = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords
    where
      wordCount : String -> Nat
      wordCount str = length (words str)
      allLengths : List String -> List Nat
      allLengths strs = map length strs

showAverage : String -> String
showAverage str = "The avareage word length is "  ++ show (average str) ++ "\n"

main : IO ()
main = repl "Enter a string: " showAverage

Types

Numbers

• Int :: fixed-width integer type

• Integer :: unbounded signed integer type

• Nat :: unbounded unsigned integer type¹

• Double :: double-precision floating-point type

Idris treats numbers as Integer by default.

Idris provides a cast function to convert between types.

Characters and strings

• Char :: character, enclosed in single quotes

• String :: string literal, enclosed in double quotes

Booleans

• True and False

The inequality operator is /=, which comes from Haskell

Functions

Functions have types.

double : Int -> Int
double x = x + x

Partial application

Idris supports partial applicationby default.

add : Int -> Int -> Int
add x y = x + y

add 2 3
-- 5 : Int, expected behavior

add 2
-- add 2 : Int -> Int

Generic functions

identity : ty -> ty
identity x = x

Generic functions with constrainted types

Consider,

doulbe : ty -> ty
double x = x + x

This would result in an error because it's not constrained to a number type. Instead, we want:

doulbe: Num ty => ty -> ty
double x = x + x

Num ty means that ty is constrained by Num types. Num is an interface, which will be covered later.

Infix number operators, like in Haskell, are actually functions:

lessThanThree : Bool
lessThanThree = (< 3)

Anonymous functions

let anonymous = (\x => x * x) 2
let anonymousWithTypes = \x : Int, y : Int => x + y

Let and where

let ... in creates a local binding in an expression, e.g. let x 50 in x + x=.

where contain local binding definitions.

pythagoras : Double -> Double -> Double
pythagoras x y = sqrt (sqaure x + square y)
where
  square : Double -> DOuble
  square x = x * x

Composite types

Tuples

Fixed sized collections.

(92, "Pages")

Lists

Any-size collection, but must be same type.

[1, 2, 3, 4]

List operators

[1, 2] ++ [3, 4] -- [1, 2, 3, 4]
1 :: [2, 3, 4] -- [1, 2, 3, 4], called "cons"

Footnotes

¹The book remarks that a Nat can only be subtracted from a larger Nat, since Nat can never be negative