1{-# LANGUAGE LinearTypes #-}
2{-# LANGUAGE UnicodeSyntax #-}
3module Linear14 where
4
5-- Inference-related behaviour. Slightly sub-optimal still.
6
7bind1 :: (d ⊸ (a ⊸ b) ⊸ c) ⊸ d ⊸ (a⊸b) ⊸ c
8bind1 b x f = b x (\a -> f a)
9
10newtype I a = I a
11
12bind2 :: (d ⊸ (a ⊸ b) ⊸ c) ⊸ d ⊸ (I a⊸b) ⊸ c
13bind2 b x f = b x (\a -> f (I a))
14
15bind3 :: (d ⊸ I (a ⊸ b) ⊸ c) ⊸ d ⊸ (a⊸b) ⊸ c
16bind3 b x f = b x (I (\a -> f a))
17
18bind4 :: (d ⊸ I ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c
19bind4 b x f = b x (I (\g -> f g))
20
21bind5 :: (d ⊸ ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c
22bind5 b x f = b x (\g -> f (\a -> g a))
23
24bind6 :: (d ⊸ I ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c
25bind6 b x f = b x (I (\g -> f (\a -> g a)))
26
27