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

module FinListNew where
class FinList x l where
toList :: l > [x]
data ZeroList x = ZeroList
data SuccList x xs = SuccList x xs
instance FinList x (ZeroList x) where
toList _ = []
instance (FinList x xs) => FinList x (SuccList x xs) where
toList (SuccList x xs) = x : toList xs
data FinList' x = forall xs. FinList x xs => FinList' xs
zl' :: x > ZeroList x
zl' _ = ZeroList
nil' :: x > FinList' x
nil' x = FinList' $ zl' x
nil :: FinList' x
nil = nil' undefined
cons :: x > FinList' x > FinList' x
cons x (FinList' xs) = FinList' $ SuccList x xs
l1 = cons 5 . cons 4 . cons 1 $ nil
lErr :: FinList' Int
lErr = cons 1 lErr
