1{-# LANGUAGE LinearTypes #-}
2{-# LANGUAGE UnicodeSyntax #-}
3{-# LANGUAGE GADTs #-}
4module Linear12 where
5
6type N a = a ⊸ ()
7
8consume :: a ⊸ N a ⊸ ()
9consume x k = k x
10
11data N' a where N :: N a ⊸ N' a
12
13data M' a where M :: M a -> M' a
14
15consume' :: a ⊸ N' a ⊸ ()
16consume' x (N k) = k x
17
18data W = W (W ⊸ ())
19
20wPlusTwo :: W ⊸ W
21wPlusTwo n = W (\(W k) -> k n)
22
23data Nat = S Nat
24
25natPlusOne :: Nat ⊸ Nat
26natPlusOne n = S n
27
28data D = D ()
29
30mkD :: () ⊸ D
31mkD x = D x
32
33data Odd = E Even
34data Even = O Odd
35
36evenPlusOne :: Even ⊸ Odd
37evenPlusOne e = E e
38
39