blob: ae3ad37536eeca3dba6391ec5aae9c73b4b3258d (
plain) (
blame)
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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module PromotedTypes where
data RevList a = RNil | RevList a :> a
data Pattern :: [*] -> * where
Nil :: Pattern '[]
Cons :: Maybe h -> Pattern t -> Pattern (h ': t)
-- Unlike (:), (:>) does not have to be quoted on type level.
data RevPattern :: RevList * -> * where
RevNil :: RevPattern RNil
RevCons :: Maybe h -> RevPattern t -> RevPattern (t :> h)
data Tuple :: (*, *) -> * where
Tuple :: a -> b -> Tuple '(a, b)
|
