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 ::
  [] 

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
λΠ>