blob: 52f0c30bb4334016ae446674b0162a538363ed93 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
data Empty
data NonEmpty
data SafeList x y where
Nil :: SafeList x Empty
Cons:: Eq x => x -> SafeList x y -> SafeList x NonEmpty
One :: Eq x => x -> SafeList x Empty -> SafeList x NonEmpty
safeHead :: SafeList x NonEmpty -> x
safeHead (Cons x _) = x
foo = Cons (3 :: Int) (Cons 6 (Cons 9 Nil))
data Dict x where
DictN :: Num x => x -> Dict x
DictE :: Eq x => x -> Dict x
data Exist where
Exist :: forall a. a -> Exist
|
