Fork me on GitHub

Idris Code Snippet

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
module Evoting

import Data.Vect
import Data.List

%default total

Name : Type
Name = String

Surname : Type
Surname = String

data Candidate = Person Name Surname
data Vote = Blank | For Candidate
data Validity = Valid Vote | Invalid

Eq Candidate where
(Person name1 surname1) == (Person name2 surname2) =
name1 == name2 && surname1 == surname2
(Person name1 surname1) /= (Person name2 surname2) =
name1 /= name2 || surname1 /= surname2

validity : List Candidate -> Vote -> Validity
validity (Nil ) __________ = Invalid
validity _________ (Blank ) = Valid Blank
validity (x :: xs) (For vote) =
if x == vote then Valid (For vote) else validity xs (For vote)

invalidate : Vect n Vote -> Vect n Validity
invalidate (Nil ) = Nil
invalidate (_ :: xs) = Invalid :: invalidate xs

election : List Candidate -> Vect n Vote -> Vect n Validity
election __________ (Nil ) = Nil
election Nil (votes ) = invalidate votes
election candidates (vote :: votes) =
validity candidates vote :: election candidates votes

candidates : List Candidate
candidates =
Person "John" "Doe" ::
Person "Jane" "Doe" ::
[]

{- Version 1: Replicate real life behaviour -}
votes : Vect 3 Vote {- We know the number of citizens -}
votes =
For (Person "Jane" "Doe") ::
For (Person "John" "Hoe") :: {- Invalid candidate -}
Blank ::
[]

Idris Code output:

Welcome to the Idris REPL!
Idris 1.0

Type checking ./evoting.idr
λΠ> election candidates votes
[Valid (For (Person "Jane" "Doe")), Invalid, Valid Blank] : Vect 3 Validity
λΠ>

References:

comments powered by Disqus