mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-20 18:21:47 +03:00
ad632d825d
It's disappointing to have to do this, but I think necessary because various issue reports have shown it to be unsound (at least as far as inference goes) and, at the very least, confusing. This patch brings us back to the basic rules of QTT. On the one hand, this makes the 1 multiplicity less useful, because it means we can't flag arguments as being used exactly once which would be useful for optimisation purposes as well as precision in the type. On the other hand, it removes some complexity (and a hack) from unification, and has the advantage of being correct! Also, I still consider the 1 multiplicity an experiment. We can still do interesting things like protocol state tracking, which is my primary motivation at least. Ideally, if the 1 multiplicity is going to be more generall useful, we'll need some kind of way of doing multiplicity polymorphism in the future. I don't think subtyping is the way (I've pretty much always come to regret adding some form of subtyping). Fixes #73 (and maybe some others).
124 lines
3.9 KiB
Idris
124 lines
3.9 KiB
Idris
module Control.Linear.LIO
|
|
|
|
||| Like `Monad`, but the action and continuation must be run exactly once
|
|
||| to ensure that the computation is linear.
|
|
public export
|
|
interface LinearBind io where
|
|
bindL : (1 _ : io a) -> (1 _ : a -> io b) -> io b
|
|
|
|
export
|
|
LinearBind IO where
|
|
bindL = io_bind
|
|
|
|
||| Required usage on the result value of a computation
|
|
public export
|
|
data Usage = None | Linear | Unrestricted
|
|
|
|
-- Not sure about this, it is a horrible hack, but it makes the notation
|
|
-- a bit nicer
|
|
public export
|
|
fromInteger : (x : Integer) -> {auto _ : Either (x = 0) (x = 1)} -> Usage
|
|
fromInteger 0 = None
|
|
fromInteger 1 = Linear
|
|
fromInteger x = Unrestricted
|
|
|
|
public export
|
|
0 ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
|
|
|
|
||| A wrapper which allows operations to state the multiplicity of the value
|
|
||| they return. For example, `L IO {use=1} File` is an IO operation which
|
|
||| returns a file that must be used exactly once.
|
|
-- This is uglier than I'd like. Perhaps multiplicity polymorphism would make
|
|
-- it neater, but we don't have that (yet?), and fortunately none of this
|
|
-- horror has to be exposed to the user!
|
|
export
|
|
data L : (io : Type -> Type) ->
|
|
{default Unrestricted use : Usage} ->
|
|
(ty : Type) -> Type where
|
|
[search ty]
|
|
-- Three separate Pures, because we need to distinguish how they are
|
|
-- used, and this is neater than a continuation.
|
|
Pure0 : (0 _ : a) -> L io {use=0} a
|
|
Pure1 : (1 _ : a) -> L io {use=1} a
|
|
PureW : a -> L io a
|
|
-- The action is always run once, and the type makes an assertion about
|
|
-- how often it's safe to use the result.
|
|
Action : (1 _ : io a) -> L io {use} a
|
|
Bind : {u_act : _} ->
|
|
(1 _ : L io {use=u_act} a) ->
|
|
(1 _ : ContType io u_act u_k a b) ->
|
|
L io {use=u_k} b
|
|
|
|
ContType io None u_k a b = (0 _ : a) -> L io {use=u_k} b
|
|
ContType io Linear u_k a b = (1 _ : a) -> L io {use=u_k} b
|
|
ContType io Unrestricted u_k a b = a -> L io {use=u_k} b
|
|
|
|
RunCont : Usage -> Type -> Type -> Type
|
|
RunCont None t b = (0 _ : t) -> b
|
|
RunCont Linear t b = (1 _ : t) -> b
|
|
RunCont Unrestricted t b = t -> b
|
|
|
|
-- The repetition here is annoying, but necessary because we don't have
|
|
-- multiplicity polymorphism. We need to look at the usage to know what the
|
|
-- concrete type of the continuation is.
|
|
runK : {use : _} ->
|
|
LinearBind io =>
|
|
(1 _ : L io {use} a) -> (1 _ : RunCont use a (io b)) -> io b
|
|
runK (Pure0 x) k = k x
|
|
runK (Pure1 x) k = k x
|
|
runK (PureW x) k = k x
|
|
runK {use = None} (Action x) k = bindL x $ \x' => k x'
|
|
runK {use = Linear} (Action x) k = bindL x $ \x' => k x'
|
|
runK {use = Unrestricted} (Action x) k = bindL x $ \x' => k x'
|
|
runK (Bind {u_act = None} act next) k = runK act (\x => runK (next x) k)
|
|
runK (Bind {u_act = Linear} act next) k = runK act (\x => runK (next x) k)
|
|
runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k)
|
|
|
|
||| Run a linear program exactly once, with unrestricted return value in the
|
|
||| underlying context
|
|
export
|
|
run : (Applicative io, LinearBind io) =>
|
|
(1 _ : L io a) -> io a
|
|
run prog = runK prog pure
|
|
|
|
export
|
|
Functor io => Functor (L io) where
|
|
map fn act = Bind act \a' => PureW (fn a')
|
|
|
|
export
|
|
Applicative io => Applicative (L io) where
|
|
pure = PureW
|
|
(<*>) f a
|
|
= f `Bind` \f' =>
|
|
a `Bind` \a' =>
|
|
PureW (f' a')
|
|
|
|
export
|
|
(Applicative m, LinearBind m) => Monad (L m) where
|
|
(>>=) a k = Bind a k
|
|
|
|
-- prioritise this one for concrete LIO, so we get the most useful
|
|
-- linearity annotations.
|
|
export %inline
|
|
(>>=) : {u_act : _} ->
|
|
LinearBind io =>
|
|
(1 _ : L io {use=u_act} a) ->
|
|
(1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b
|
|
(>>=) = Bind
|
|
|
|
export %inline
|
|
pure0 : (0 x : a) -> L io {use=0} a
|
|
pure0 = Pure0
|
|
|
|
export %inline
|
|
pure1 : (1 x : a) -> L io {use=1} a
|
|
pure1 = Pure1
|
|
|
|
export
|
|
(LinearBind io, HasIO io) => HasIO (L io) where
|
|
liftIO p = Action (liftIO p)
|
|
|
|
public export
|
|
LinearIO : (Type -> Type) -> Type
|
|
LinearIO io = (LinearBind io, HasIO io)
|