Programming in Idris

Implicit Argument

 
xxxxxxxxxx
11
1
-- explicit
2
append: (elem: Type) -> (n: Nat) -> (m: Nat) ->
3
    Vect n elem -> Vect m elem -> Vect (n + m) elem
4
-- > append Char 2 2 ['a', 'b'] ['c', 'd']
5
-- > append _ _ _ ['a', 'b'] ['c', 'd']
6
​
7
-- implicit
8
append: Vect n elem -> Vect m elem -> Vect (n + m) elem   -- unbound
9
append: {elem: Type} -> {n: Nat} -> {m: Nat} ->
10
    Vect n elem -> Vect m elem -> Vect (n + m) elem   -- bound
11
-- > append ['a', 'b'] ['c', 'd']

Use Implicit in Function

 
xxxxxxxxxx
13
1
-- plain
2
length: Vect n elem -> Nat
3
length [] = Z
4
length (x :: xs) = 1 + length xs
5
​
6
-- dependent
7
length: Vect n elem -> Nat
8
length {n} xs = n
9
​
10
-- dependent with pattern matching
11
createEmpties: Vect n (Vect 0 a)
12
createEmpties {n = Z} = []
13
createEmpties {n = (S k)} = [] :: createEmpties

Basic Data Types

 
xxxxxxxxxx
20
1
-- enumerated types (enum)
2
data Bool = False | True
3
data Direction = North | East | South | West
4
​
5
-- union types (parameterized enum)
6
data Shape = Triangle Double Double
7
      | Rectangle Double Double
8
      | Circle Double
9
data Shape: Type where
10
  Triangle: Double -> Double -> Shape
11
  Rectangle: Double -> Double -> Shape
12
  Circle: Double -> Shape
13
      
14
-- recursive types (self-defining types)
15
data Nat = Z | S Nat
16
data Infinite = Forever Infinite
17
​
18
-- generic types (type-parameterized)
19
data Maybe valtype = Nothing | Just valtype
20
data Either a b = Left a | Right b

Pattern Naming and Reuse

 
xxxxxxxxxx
5
1
insert x orig@(Node left val right)
2
  = case compare x val of
3
    LT => Node (insert x left) val right
4
    EQ => orig
5
    GT => Node left val (insert x right)

Dependent Data Types

 
xxxxxxxxxx
15
1
data PowerSouce = Petrol | Pedal
2
​
3
data Vehicle: PowerSource -> Type where   -- dependent types / families of types
4
  Bicycle: Vehicle Pedal
5
  Car: (fuel: Nat) -> Vehicle Petrol
6
  Bus: (fuel: Nat) -> Vehicle Petrol
7
  
8
data Vect: Nat -> Type -> Type where
9
  Nil: Vect Z a
10
  (::): (x: a) -> (xs: Vect k a) -> Vect (S k) a
11
  
12
data DataStore: Type where
13
  MkData: (size: Nat) ->
14
        (items: Vect size String) ->  -- computation from parameters
15
        DataStore

Dependent Pairs

 
xxxxxxxxxx
2
1
anyVect: (n: Nat ** Vect n String)    -- second element computed from the first
2
anyVect: (n ** Vect n String)     -- type inference

Type-level Calculation

 
x
1
  -- type calculation functions
2
StringOrInt: Bool -> Type
3
StringOrInt False = String
4
StringOrInt True = Int
5
-- usage
6
getStringOrInt: (isInt: Bool) -> StringOrInt isInt
7
getStringOrInt False = "Ninety Four"
8
getStringOrInt True = 94
9
​
10
-- or use case expression directly
11
valToString': (isInt: Bool) -> (case isInt of False => String True => Int) -> String
12
valToString' False y = trim y
13
valToString' True y = cast y

Interfaces

 
xxxxxxxxxx
14
1
Eq Matter where
2
    (==) Solid Solid = True
3
    (==) Liquid Liquid = True
4
    (==) Gas Gas = True
5
    (==) _ _ = False
6
    
7
    (/=) x y = not (x == y)
8
    
9
-- default methods
10
interface Eq a where
11
    (==): a -> a -> Bool
12
    (/=): a -> a -> Bool
13
    
14
    (==) x y = not (x /= y)
15
    (/=) x y = not (x == y)