blob: 14b29170b1f8cd96f6719db5868fa1aa2ed75445 (
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
|
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module A where
infixr 7 :*
infix 8 :*:
data HNil
data α :* β
type HSingle α = α :* HNil
type α :*: β = α :* β :* HNil
data HList l where
HNil ∷ HList HNil
(:*) ∷ α → HList t → HList (α :* t)
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
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
|
