blob: 5b2ff393466f3eb1d9bcb47965b170152879d72a (
plain)
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
infixr 7 :*, .*
infix 8 :*:, .*.
data HNil
data α :* β
type HSingle α = α :* HNil
type α :*: β = α :* β :* HNil
data HList l where
HNil ∷ HList HNil
(:*) ∷ α → HList t → HList (α :* t)
(.*) ∷ α → HList t → HList (α :* t)
(.*) = (:*)
(.*.) ∷ α → β → HList (α :*: β)
a .*. b = a .* b .* HNil
data First
data Next p
data HIndex i where
First ∷ HIndex First
Next ∷ HIndex p → HIndex (Next p)
class (l ~ (HHead l :* HTail l)) ⇒ HNonEmpty l where
type HHead l
type HTail l
instance HNonEmpty (h :* t) where
type HHead (h :* t) = h
type HTail (h :* t) = t
hHead ∷ HNonEmpty l ⇒ HList l → HHead l
hHead (h :* _) = h
hHead _ = undefined
hTail ∷ HNonEmpty l ⇒ HList l → HList (HTail l)
hTail (_ :* t) = t
hTail _ = undefined
data HFromWitness n l where
HFromFirst ∷ HFromWitness First l
HFromNext ∷ (HNonEmpty l, HFromClass p (HTail l),
HTail (HFrom (Next p) l) ~ HFrom (Next p) (HTail l))
⇒ HFromWitness (Next p) l
class HFromClass n l where
type HFrom n l
hFromWitness ∷ HFromWitness n l
instance HFromClass First l where
type HFrom First l = l
hFromWitness = HFromFirst
instance (HNonEmpty l, HFromClass p (HTail l)) ⇒ HFromClass (Next p) l where
type HFrom (Next p) l = HFrom p (HTail l)
hFromWitness = case hFromWitness ∷ HFromWitness p (HTail l) of
HFromFirst → HFromNext
HFromNext → HFromNext
hFrom ∷ ∀ n l . HFromClass n l ⇒ HIndex n → HList l → HList (HFrom n l)
hFrom First l = l
hFrom (Next p) l = case hFromWitness ∷ HFromWitness n l of
HFromNext → hFrom p (hTail l)
_ → undefined
type HNth n l = HHead (HFrom n l)
hNth ∷ ∀ n l . (HFromClass n l, HNonEmpty (HFrom n l))
⇒ HIndex n → HList l → HNth n l
hNth First l = hHead l
hNth (Next p) l = case hFromWitness ∷ HFromWitness n l of
HFromNext → hNth p (hTail l)
_ → undefined
main = putStrLn $ hNth (Next First) (0 .*. "Test")
|
