mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-19 10:51:35 +03:00
413d09dad8
We've been generalising inferred function types to have multiplicity RigW but sometimes (especially on lambdas) we need to infer the precise type, so make a distinction. This is pretty ugly, really. It would be better to be able to postpone the choice until we know more, but it's not obvious to me how to achieve that with the way unification is currently set up. The present way at least works fine with code that doesn't use linearity, which is the right default I think!
85 lines
2.0 KiB
Idris
85 lines
2.0 KiB
Idris
module Linear
|
|
|
|
public export
|
|
data Usage = Once | Many
|
|
|
|
public export
|
|
data Lin : (Type -> Type) -> Usage -> Type -> Type where
|
|
Pure : (1 x : a) -> Lin m usage a
|
|
Lift : (1 x : m a) -> Lin m Many a
|
|
BindOnce : (1 act : Lin m Once a) ->
|
|
(1 k : (1 x : a) -> Lin m t b) -> Lin m t b
|
|
BindMany : (1 act : Lin m Many a) ->
|
|
(1 k : (x : a) -> Lin m t b) -> Lin m t b
|
|
|
|
public export
|
|
data Unrestricted : Type -> Type where
|
|
MkUn : (x : a) -> Unrestricted a
|
|
|
|
export
|
|
pure : (1 x : a) -> Lin m usage a
|
|
pure = Pure
|
|
|
|
export
|
|
lift : (1 x : m a) -> Lin m Many a
|
|
lift = Lift
|
|
|
|
public export
|
|
contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
|
|
contType m Once q a b = (1 x : a) -> Lin m q b
|
|
contType m Many q a b = (x : a) -> Lin m q b
|
|
|
|
public export
|
|
(>>=) : {p : _} ->
|
|
(1 f : Lin m p a) -> (1 k : contType m p q a b) -> Lin m q b
|
|
(>>=) {p=Once} = BindOnce
|
|
(>>=) {p=Many} = BindMany
|
|
|
|
export
|
|
run : Monad m => Lin m usage t -> m t
|
|
run (Pure x) = pure x
|
|
run (Lift p) = p
|
|
run (BindOnce act k)
|
|
= do act' <- run act
|
|
run (k act')
|
|
run (BindMany act k)
|
|
= do act' <- run act
|
|
run (k act')
|
|
|
|
public export
|
|
One : (Type -> Type) -> Type -> Type
|
|
One m = Lin m Once
|
|
|
|
public export
|
|
Any : (Type -> Type) -> Type -> Type
|
|
Any m = Lin m Many
|
|
|
|
infix 2 @@
|
|
|
|
public export
|
|
data Res : (a : Type) -> (a -> Type) -> Type where
|
|
(@@) : (val : a) -> (1 resource : r val) -> Res a r
|
|
|
|
|
|
{-
|
|
data DoorState = Closed | Open
|
|
|
|
data Door : DoorState -> Type where
|
|
MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)
|
|
|
|
newDoor : One m (Door Closed)
|
|
knock : (1 d : Door t) -> One m (Door t)
|
|
openDoor : (1 d : Door Closed) -> One m (Res Bool (\ok => Door (if ok then Open else Closed)))
|
|
closeDoor : (1 d : Door Open) -> One m (Door Closed)
|
|
deleteDoor : (1 d : Door Closed) -> Any m ()
|
|
|
|
doorProg : Any m ()
|
|
doorProg
|
|
= do d <- newDoor
|
|
ok @@ d' <- openDoor d
|
|
d'' <- knock d'
|
|
if ok
|
|
then ?doorOK
|
|
else ?doorBad
|
|
-}
|