#+title: Type-Driven Development With Idris
- source ::

Note: code for this book in [[file:../20210713213112-idris2.org][Idris2]] can be found [[https://github.com/edwinb/Idris2/tree/master/tests/typedd-book][here]].

* 1. Overview
[[file:../20210423133247-type_driven_development.org][Type-driven development]] could be thought of as designing the [[file:../20210423133319-type_programming.org][types]] for 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 [[file:../20210423171911-concurrent_programming.org][concurrent programming]] by 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:

|           | Input 1 type | Input 2 type | Output type       |
|-----------+--------------+--------------+-------------------|
| Simple    | AnyList      | AnyList      | AnyList           |
| Generic   | List elem    | List elem    | List elem         |
| Dependent | Vect n elem  | Vect m elem  | Vect (n + m) elem |

[[file:../20210607154159-idris.org][Idris]] is a [[file:../20210607154216-pure_functional_programming.org][pure functional programming]] language.

- [[file:../20200604222704-functional_programming.org][functional programming]] :: programs are composed of first class functional
  constructs, and program execution consists of evaluating those functions
- [[file:../20210607154216-pure_functional_programming.org][pure functional programming]] :: in addition to functional programming,
  functions do not have [[file:../20210607155229-side_effect.org][side-effects]] and all functions are [[file:../20210607154420-idempotency.org][idempotency]]

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

- [[file:../20210607202511-referential_transparency.org][referential transparency]] :: the property of a function to produce the same
  output as an input. A key to [[file:../20210607154216-pure_functional_programming.org][pure functional programming]]

In [[file:../20210607154159-idris.org][Idris]], a [[file:../20210516170353-data_type.org][type]] that describes a [[file:../20210607155229-side_effect.org][side-effect]] is denoted as such, e.g. =String=
vs. =IO String=.

- [[file:../20210607210239-total_function.org][total function]] :: a function that always returns a result
- [[file:../20210516164317-partial_function.org][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:

#+begin_src idris
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
#+end_src
** Types
*** Numbers
- Int :: /fixed-width/ integer type
- Integer :: /unbounded/ signed integer type
- Nat :: /unbounded/ unsigned integer type[fn:1]
- 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 [[file:../20200708123930-haskell.org][Haskell]].
** Functions
Functions have types.

#+begin_src idris
double : Int -> Int
double x = x + x
#+end_src
*** Partial application
Idris supports [[file:../20210607203034-partial_application.org][partial application]] by default.

#+begin_src idris
add : Int -> Int -> Int
add x y = x + y

add 2 3
-- 5 : Int, expected behavior

add 2
-- add 2 : Int -> Int
#+end_src
*** Generic functions
#+begin_src idris
identity : ty -> ty
identity x = x
#+end_src
*** Generic functions with constrainted types
Consider,
#+begin_src idris
doulbe : ty -> ty
double x = x + x
#+end_src

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

#+begin_src idris
doulbe: Num ty => ty -> ty
double x = x + x
#+end_src

=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:

#+begin_src idris
lessThanThree : Bool
lessThanThree = (< 3)
#+end_src
*** Anonymous functions
#+begin_src idris
let anonymous = (\x => x * x) 2
let anonymousWithTypes = \x : Int, y : Int => x + y
#+end_src
*** =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.

#+begin_src idris
pythagoras : Double -> Double -> Double
pythagoras x y = sqrt (sqaure x + square y)
where
  square : Double -> DOuble
  square x = x * x
#+end_src
** Composite types
*** Tuples
Fixed sized collections.

#+begin_src
(92, "Pages")
#+end_src
*** Lists
Any-size collection, but must be same type.

#+begin_src
[1, 2, 3, 4]
#+end_src
**** List operators
#+begin_src
[1, 2] ++ [3, 4] -- [1, 2, 3, 4]
1 :: [2, 3, 4] -- [1, 2, 3, 4], called "cons"
#+end_src

* Footnotes
[fn:1] The book remarks that a =Nat= can only be subtracted from a larger =Nat=,
since =Nat= can never be negative