0 | module Data.Linear.LMaybe
 1 |
 2 | import Data.Linear.Bifunctor
 3 | import Data.Linear.Interface
 4 | import Data.Linear.Notation
 5 |
 6 | %default total
 7 |
 8 | ||| Linear version of Maybe
 9 | public export
10 | data LMaybe : Type -> Type where
11 |   Nothing : LMaybe a
12 |   Just : a -@ LMaybe a
13 |
14 | export
15 | (<$>) : (a -@ b) -> LMaybe a -@ LMaybe b
16 | f <$> Nothing = Nothing
17 | f <$> Just x = Just (f x)
18 |
19 | export
20 | Consumable a => Consumable (LMaybe a) where
21 |   consume Nothing = ()
22 |   consume (Just a) = consume a
23 |
24 | export
25 | Duplicable a => Duplicable (LMaybe a) where
26 |   duplicate Nothing = [Nothing, Nothing]
27 |   duplicate (Just a) = Just <$> duplicate a
28 |