Idris code snippets

idris_cookbook.md

Idris Cookbook

From Haskell

newtype

newtype WorldM a = WorldM { asT :: WorldT a }

record WorldM (a : Type) where
  constructor MkWorldM
  asT : WorldT a

Nested loops

foo : Nat -> Nat -> IO ()
foo height width =
  do
    let j : Nat = height
    outerLoop j
  where
    innerLoop : (j : Nat) -> (i : Nat) -> IO ()
    innerLoop _ Z = pure ()
    innerLoop j (S i) =
      do
        let i' : Nat = minus width (plus i 1)
        putStrLn $ printf "i':%d, j:%d" (cast i') (cast j)
        innerLoop j i

    outerLoop : Nat -> IO ()
    outerLoop Z = pure ()
    outerLoop (S j) =
      do
        innerLoop j width
        outerLoop j

Random doubles

import Effects
import Effect.Random

RAND_MAX : Integer
RAND_MAX = 32767

randomUnitDouble : Eff Double [RND]
randomUnitDouble =
  pure $ (fromInteger !(rndInt 0 RAND_MAX)) / (1.0 + (fromInteger RAND_MAX))

randomDouble : (min : Double) -> (max : Double) -> Eff Double [RND]
randomDouble min max =
    pure $ (min + (max - min) * !randomUnitDouble)

Testing

test : IO (Double)
test =
  do
    pure $ runPure (randomDouble (-100) 100)

Custom data types

Basics

Data types are defined by a type constructor and one or more data constructors.

Type synonyms

RGB : Type
RGB = Vect 3 Bits8

-- with type-level variables
Matrix : (rows : Nat) -> (cols: Nat) -> Type
Matrix rows cols = Vect rows (Vect cols Double)

-- used in other type synonyms
SquareMatrix : (n : Nat) -> Type
SquareMatrix n = Matrix n n

Enumerations

data Bool = True | False

-- OR

data Bool : Type where
  True : Bool
  False : Bool

Unions

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

-- OR

data Shape : Type where
  Triangle : Double -> Double -> Shape
  Rectangle : Double -> Double -> Shape
  Circle : Double -> Shape

Recursive

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

-- OR

data Picture : Type where
  Primitive : Shape -> Picture
  Combine : Picture -> Picture -> Picture
  Rotate : Double -> Picture -> Picture
  Translate : Double -> Double -> Picture -> Picture

Generic

data Maybe valtype = Nothing
                   | Just valtype

-- OR

data Maybe : valtype -> Type where
  Nothing : Maybe valtype
  Just : valtype -> Maybe valtype
  
-- multiple type-level variables
data Either a b = Left a | Right b

-- OR

data Either : a -> b -> Type where
  Left : a -> Either a b
  Right : b -> Either a b

Records

data DataStore : Type where
  MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : DataStore -> Nat
size (MkData size' _) = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData _ items') = items'

-- OR

record DataStore where
  constructore MkData
  size : Nat
  items : Vect size String  

Interfaces

interface C (t : Type) where
  m : t

data A = B

implementation C A where
  m = B

-- > E {a=Int} {b=String}
--   E : D Int String
data D a b = E

implementation C (D a b) where
  m = E

Advanced

Named implementations

See Named Implementations

Determining parameters

See Determining Parameters

interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) | m where {}

Retaining types in interfaces in new structures

Define an Abstract interface and one Concrete instance:

interface Abstract a where
  fooAbstract : a -> Bool

record Concrete where
  constructor MkConcrete
  fooConcrete : Bool

Abstract Concrete where
  fooAbstract = fooConcrete

Use this in a simple function:

baz : Abstract a => a -> Bool
baz abstract = fooAbstract abstract

Define a Thing to hold any valid Abstract field:

data Thing : Type -> Type where
  MkThing : (abstract : a) -> Abstract a => Thing a

Use whatever Abstract is associated with a Thing:

abstract : Abstract b => Thing b -> b
abstract (MkThing b) = b

(This is an accessor, but it could be any function that needs an instance of Abstract.)

c1 : Concrete
c1 = MkConcrete True

t1 : Thing Concrete
t1 = MkThing c1

> abstract t1
MkConcrete True : Concrete

Records

record Person (age : Nat) where
  constructor MkPerson
  name : String

record Event where
  constructor MkEvent
  name : String
  organiser : Person a

record Meeting (year : Int) where
  constructor MkMeeting
  event : Event
  organiser : Person a

new_organiser : String -> List (Meeting x) -> List (Meeting x)
new_organiser n = map (record { event->organiser->name = n }) 

next_year : Meeting x -> Meeting (x+1)
next_year m = record { organiser->param_age
                          = record { organiser->param_age } m + 1,
                       event->organiser->param_age
                          = record { event->organiser->param_age } m + 1,
                       param_year = _ } m

fred : Person 20
fred = MkPerson "Fred"

jim : Person 29
jim = MkPerson {age=29} "Jim"

idm : Event
idm = MkEvent "Idris Developers Meeting" fred

idm_gbg : Meeting 2014
idm_gbg = MkMeeting idm jim

test : Meeting 2015
test = next_year idm_gbg

main : IO ()
main = do printLn (record { event->organiser->name } test)
          printLn (record { event->organiser->param_age } test)
          printLn (record { event->organiser->param_age } idm_gbg)
          printLn (record { organiser->param_age } test)
          printLn (record { organiser->param_age } idm_gbg)
          printLn (record { param_year } idm_gbg)