blob: 3f49e949487c36a406c0d1fc44d6405e4954a0f5 (
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
|
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE GADTs #-}
module Linear12 where
type N a = a ⊸ ()
consume :: a ⊸ N a ⊸ ()
consume x k = k x
data N' a where N :: N a ⊸ N' a
consume' :: a ⊸ N' a ⊸ ()
consume' x (N k) = k x
data W = W (W ⊸ ())
wPlusTwo :: W ⊸ W
wPlusTwo n = W (\(W k) -> k n)
data Nat = S Nat
natPlusOne :: Nat ⊸ Nat
natPlusOne n = S n
data D = D ()
mkD :: () ⊸ D
mkD x = D x
data Odd = E Even
data Even = O Odd
evenPlusOne :: Even ⊸ Odd
evenPlusOne e = E e
|
