blob: 624f9d5ad8dd471d41851f4e3a5dbf2f5e62d642 (
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
26
|
{-# LANGUAGE Haskell2010 #-}
{-# 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)
|
