mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-20 01:37:35 +03:00
[ linear ] These seem useful (#2316)
This commit is contained in:
parent
bec4a0a88e
commit
33d99adb53
@ -17,6 +17,22 @@ Consumable Void where consume v impossible
|
|||||||
|
|
||||||
export
|
export
|
||||||
Consumable () where consume u = u
|
Consumable () where consume u = u
|
||||||
|
|
||||||
|
||| Unions can be consumed by pattern matching
|
||||||
|
export
|
||||||
|
Consumable Bool where
|
||||||
|
consume True = ()
|
||||||
|
consume False = ()
|
||||||
|
|
||||||
|
export
|
||||||
|
Consumable (!* a) where
|
||||||
|
consume (MkBang v) = ()
|
||||||
|
|
||||||
|
||| We can cheat to make built-in types consumable
|
||||||
|
export
|
||||||
|
Consumable Int where
|
||||||
|
consume = believe_me (\ 0 i : Int => ())
|
||||||
|
|
||||||
-- But crucially we don't have `Consumable World` or `Consumable Handle`.
|
-- But crucially we don't have `Consumable World` or `Consumable Handle`.
|
||||||
|
|
||||||
infixr 5 `seq`
|
infixr 5 `seq`
|
||||||
@ -27,29 +43,27 @@ export
|
|||||||
seq : Consumable a => a -@ b -@ b
|
seq : Consumable a => a -@ b -@ b
|
||||||
a `seq` b = let 1 () = consume a in b
|
a `seq` b = let 1 () = consume a in b
|
||||||
|
|
||||||
||| Unions can be consumed by pattern matching
|
|
||||||
export
|
|
||||||
Consumable Bool where
|
|
||||||
consume True = ()
|
|
||||||
consume False = ()
|
|
||||||
|
|
||||||
||| We can cheat to make built-in types consumable
|
|
||||||
export
|
|
||||||
Consumable Int where
|
|
||||||
consume = believe_me (\ 0 i : Int => ())
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
interface Duplicable a where
|
interface Duplicable a where
|
||||||
duplicate : (1 v : a) -> 2 `Copies` v
|
duplicate : (1 v : a) -> 2 `Copies` v
|
||||||
|
|
||||||
export
|
export
|
||||||
Duplicable Void where
|
Duplicable Void where
|
||||||
duplicate Void impossible
|
duplicate v impossible
|
||||||
|
|
||||||
export
|
export
|
||||||
Duplicable () where
|
Duplicable () where
|
||||||
duplicate () = [(), ()]
|
duplicate () = [(), ()]
|
||||||
|
|
||||||
|
export
|
||||||
|
Duplicable Bool where
|
||||||
|
duplicate True = [True, True]
|
||||||
|
duplicate False = [False, False]
|
||||||
|
|
||||||
|
export
|
||||||
|
Duplicable (!* a) where
|
||||||
|
duplicate (MkBang v) = [MkBang v, MkBang v]
|
||||||
|
|
||||||
||| Comonoid is the dual of Monoid, it can consume a value linearly and duplicate a value linearly
|
||| Comonoid is the dual of Monoid, it can consume a value linearly and duplicate a value linearly
|
||||||
||| `comult` returns a pair instead of 2 copies, because we do not guarantee that the two values
|
||| `comult` returns a pair instead of 2 copies, because we do not guarantee that the two values
|
||||||
||| are identical, unlike with `duplicate`. For example if we build a comonoid out of a group, with
|
||| are identical, unlike with `duplicate`. For example if we build a comonoid out of a group, with
|
||||||
@ -64,7 +78,7 @@ interface Comonoid a where
|
|||||||
|
|
||||||
||| If a value is consumable and duplicable we can make an instance of Comonoid for it
|
||| If a value is consumable and duplicable we can make an instance of Comonoid for it
|
||||||
export
|
export
|
||||||
Consumable a => Duplicable a => Comonoid a where
|
[AutoComonoid] Consumable a => Duplicable a => Comonoid a where
|
||||||
counit = consume
|
counit = consume
|
||||||
comult x = pair (duplicate x)
|
comult x = pair (duplicate x)
|
||||||
|
|
||||||
@ -72,4 +86,3 @@ export
|
|||||||
Comonoid (!* a) where
|
Comonoid (!* a) where
|
||||||
counit (MkBang _) = ()
|
counit (MkBang _) = ()
|
||||||
comult (MkBang v) = MkBang v # MkBang v
|
comult (MkBang v) = MkBang v # MkBang v
|
||||||
|
|
||||||
|
@ -1,5 +1,7 @@
|
|||||||
module Data.Linear.LVect
|
module Data.Linear.LVect
|
||||||
|
|
||||||
|
import Data.Fin
|
||||||
|
|
||||||
import Data.Linear.Bifunctor
|
import Data.Linear.Bifunctor
|
||||||
import Data.Linear.Interface
|
import Data.Linear.Interface
|
||||||
import Data.Linear.Notation
|
import Data.Linear.Notation
|
||||||
@ -15,6 +17,11 @@ data LVect : Nat -> Type -> Type where
|
|||||||
|
|
||||||
%name LVect xs, ys, zs, ws
|
%name LVect xs, ys, zs, ws
|
||||||
|
|
||||||
|
export
|
||||||
|
lookup : Fin (S n) -@ LVect (S n) a -@ LPair a (LVect n a)
|
||||||
|
lookup FZ (v :: vs) = (v # vs)
|
||||||
|
lookup (FS k) (v :: vs@(_ :: _)) = bimap id (v ::) (lookup k vs)
|
||||||
|
|
||||||
export
|
export
|
||||||
(<$>) : (f : a -@ b) -> LVect n a -@ LVect n b
|
(<$>) : (f : a -@ b) -> LVect n a -@ LVect n b
|
||||||
f <$> [] = []
|
f <$> [] = []
|
||||||
@ -50,6 +57,20 @@ export
|
|||||||
[] ++ ys = ys
|
[] ++ ys = ys
|
||||||
(x :: xs) ++ ys = x :: (xs ++ ys)
|
(x :: xs) ++ ys = x :: (xs ++ ys)
|
||||||
|
|
||||||
|
export
|
||||||
|
lfoldr : (0 p : Nat -> Type) -> (forall n. a -@ p n -@ p (S n)) -> p Z -@ LVect n a -@ p n
|
||||||
|
lfoldr p c n [] = n
|
||||||
|
lfoldr p c n (x :: xs) = c x (lfoldr p c n xs)
|
||||||
|
|
||||||
|
export
|
||||||
|
lfoldl : (0 p : Nat -> Type) -> (forall n. a -@ p n -@ p (S n)) -> p Z -@ LVect n a -@ p n
|
||||||
|
lfoldl p c n [] = n
|
||||||
|
lfoldl p c n (x :: xs) = lfoldl (p . S) c (c x n) xs
|
||||||
|
|
||||||
|
export
|
||||||
|
reverse : LVect m a -@ LVect m a
|
||||||
|
reverse = lfoldl (\ m => LVect m a) (::) []
|
||||||
|
|
||||||
export
|
export
|
||||||
Consumable a => Consumable (LVect n a) where
|
Consumable a => Consumable (LVect n a) where
|
||||||
consume [] = ()
|
consume [] = ()
|
||||||
|
10
libs/linear/Data/Linear/List/LQuantifiers.idr
Normal file
10
libs/linear/Data/Linear/List/LQuantifiers.idr
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
module Data.Linear.List.LQuantifiers
|
||||||
|
|
||||||
|
import Data.Linear.Notation
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
public export
|
||||||
|
data LAll : (p : a -> Type) -> List a -> Type where
|
||||||
|
Nil : LAll p []
|
||||||
|
(::) : p x -@ LAll p xs -@ LAll p (x :: xs)
|
@ -8,6 +8,11 @@ public export
|
|||||||
(-@) : Type -> Type -> Type
|
(-@) : Type -> Type -> Type
|
||||||
a -@ b = (1 _ : a) -> b
|
a -@ b = (1 _ : a) -> b
|
||||||
|
|
||||||
|
||| Linear identity function
|
||||||
|
public export
|
||||||
|
id : a -@ a
|
||||||
|
id x = x
|
||||||
|
|
||||||
||| Linear function composition
|
||| Linear function composition
|
||||||
public export
|
public export
|
||||||
(.) : (b -@ c) -@ (a -@ b) -@ (a -@ c)
|
(.) : (b -@ c) -@ (a -@ b) -@ (a -@ c)
|
||||||
|
@ -9,8 +9,8 @@ modules = Data.Linear,
|
|||||||
Data.Linear.Interface,
|
Data.Linear.Interface,
|
||||||
Data.Linear.LEither,
|
Data.Linear.LEither,
|
||||||
Data.Linear.LList,
|
Data.Linear.LList,
|
||||||
|
Data.Linear.List.LQuantifiers,
|
||||||
Data.Linear.LMaybe,
|
Data.Linear.LMaybe,
|
||||||
Data.Linear.LNat,
|
Data.Linear.LNat,
|
||||||
Data.Linear.LVect,
|
Data.Linear.LVect,
|
||||||
Data.Linear.Notation
|
Data.Linear.Notation
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user