{-# LANGUAGE GADTs #-} module AsyncRattus.InternalPrimitives where import Prelude hiding (Left, Right) import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet -- An input channel is identified by an integer. The programmer should not know about it. type InputChannelIdentifier = Int type Clock = IntSet singletonClock :: InputChannelIdentifier -> Clock singletonClock :: InputChannelIdentifier -> Clock singletonClock = InputChannelIdentifier -> Clock IntSet.singleton clockUnion :: Clock -> Clock -> Clock clockUnion :: Clock -> Clock -> Clock clockUnion = Clock -> Clock -> Clock IntSet.union channelMember :: InputChannelIdentifier -> Clock -> Bool channelMember :: InputChannelIdentifier -> Clock -> Bool channelMember = InputChannelIdentifier -> Clock -> Bool IntSet.member data InputValue where InputValue :: !InputChannelIdentifier -> !a -> InputValue -- | The "later" type modality. A value @v@ of type @O 𝜏@ consists of -- two components: Its clock, denoted @cl(v)@, and a delayed -- computation that will produce a value of type @𝜏@ as soon as the -- clock @cl(v)@ ticks. The clock @cl(v)@ is only used for type -- checking and is not directly accessible, whereas the delayed -- computation is accessible via 'adv' and 'select'. data O a = Delay !Clock (InputValue -> a) -- | The return type of the 'select' primitive. data Select a b = Fst !a !(O b) | Snd !(O a) !b | Both !a !b asyncRattusError :: [Char] -> a asyncRattusError [Char] pr = forall a. HasCallStack => [Char] -> a error ([Char] pr forall a. [a] -> [a] -> [a] ++ [Char] ": Did you forget to mark this as Async Rattus code?") -- | This is the constructor for the "later" modality 'O': -- -- > Γ ✓θ ⊢ t :: 𝜏 -- > -------------------- -- > Γ ⊢ delay t :: O 𝜏 -- -- The typing rule requires that its argument @t@ typecheck with an -- additional tick @✓θ@ of some clock @θ@. {-# INLINE [1] delay #-} delay :: a -> O a delay :: forall a. a -> O a delay a _ = forall {a}. [Char] -> a asyncRattusError [Char] "delay" extractClock :: O a -> Clock extractClock :: forall a. O a -> Clock extractClock (Delay Clock cl InputValue -> a _) = Clock cl {-# INLINE [1] adv' #-} adv' :: O a -> InputValue -> a adv' :: forall a. O a -> InputValue -> a adv' (Delay Clock _ InputValue -> a f) InputValue inp = InputValue -> a f InputValue inp -- | This is the eliminator for the "later" modality 'O': -- -- > Γ ⊢ t :: O 𝜏 Γ' tick-free -- > --------------------------------- -- > Γ ✓cl(t) Γ' ⊢ adv t :: 𝜏 -- -- It requires that a tick @✓θ@ is in the context whose clock matches -- exactly the clock of @t@, i.e. @θ = cl(t)@. {-# INLINE [1] adv #-} adv :: O a -> a adv :: forall a. O a -> a adv O a _ = forall {a}. [Char] -> a asyncRattusError [Char] "adv" -- | If we want to eliminate more than one delayed computation, i.e.\ -- two @s :: O σ@ and @t :: O 𝜏@, we need to use 'select' instead of -- just 'adv'. -- -- > Γ ⊢ s :: O σ Γ ⊢ t :: O 𝜏 Γ' tick-free -- > -------------------------------------------------- -- > Γ ✓cl(s)⊔cl(t) Γ' ⊢ select s t :: Select σ 𝜏 -- -- It requires that we have a tick @✓θ@ in the context whose clock -- matches the union of the clocks of @s@ and @t@, i.e. @θ = -- cl(s)⊔cl(t)@. The union of two clocks ticks whenever either of the -- two clocks ticks, i.e. @cl(s)⊔cl(t)@, whenever @cl(s)@ or @cl(t)@ -- ticks. -- -- That means there are three possible outcomes, which are reflected -- in the result type of @select s t@. A value of @Select σ 𝜏@ is -- either -- -- * a value of type @σ@ and a delayed computation of type @O 𝜏@, if -- @cl(s)@ ticks before @cl(t)@, -- -- * a value of type @𝜏@ and a delayed computation of type @O σ@, if -- @cl(t)@ ticks before @cl(s)@, or -- -- * a value of type @σ@ and a value of type @𝜏@, if @cl(s)@ and -- * @cl(s)@ tick simultaneously. {-# INLINE [1] select #-} select :: O a -> O b -> Select a b select :: forall a b. O a -> O b -> Select a b select O a _ O b _ = forall {a}. [Char] -> a asyncRattusError [Char] "select" select' :: O a -> O b -> InputValue -> Select a b select' :: forall a b. O a -> O b -> InputValue -> Select a b select' a :: O a a@(Delay Clock clA InputValue -> a inpFA) b :: O b b@(Delay Clock clB InputValue -> b inpFB) inputValue :: InputValue inputValue@(InputValue InputChannelIdentifier chId a _) = if InputChannelIdentifier chId InputChannelIdentifier -> Clock -> Bool `channelMember` Clock clA then if InputChannelIdentifier chId InputChannelIdentifier -> Clock -> Bool `channelMember` Clock clB then forall a b. a -> b -> Select a b Both (InputValue -> a inpFA InputValue inputValue) (InputValue -> b inpFB InputValue inputValue) else forall a b. a -> O b -> Select a b Fst (InputValue -> a inpFA InputValue inputValue) O b b else forall a b. O a -> b -> Select a b Snd O a a (InputValue -> b inpFB InputValue inputValue) -- | The clock of @never :: O 𝜏@ will never tick, i.e. it will never -- produce a value of type @𝜏@. With 'never' we can for example -- implement the constant signal @x ::: never@ of type @Sig a@ for any @x :: -- a@. never :: O a never :: forall a. O a never = forall a. Clock -> (InputValue -> a) -> O a Delay Clock IntSet.empty (forall a. HasCallStack => [Char] -> a error [Char] "Trying to adv on the 'never' delayed computation") -- | A type is @Stable@ if it is a strict type and the later modality -- @O@ and function types only occur under @Box@. -- -- For example, these types are stable: @Int@, @Box (a -> b)@, @Box (O -- Int)@, @Box (Sig a -> Sig b)@. -- -- But these types are not stable: @[Int]@ (because the list type is -- not strict), @Int -> Int@, (function type is not stable), @O -- Int@, @Sig Int@. class Stable a where -- | The "stable" type modality. A value of type @Box a@ is a -- time-independent computation that produces a value of type @a@. -- Use 'box' and 'unbox' to construct and consume 'Box'-types. data Box a = Box a -- | This is the constructor for the "stable" modality 'Box': -- -- > Γ☐ ⊢ t :: 𝜏 -- > -------------------- -- > Γ ⊢ box t :: Box 𝜏 -- -- where Γ☐ is obtained from Γ by removing all ticks and all variables -- @x :: 𝜏@, where 𝜏 is not a stable type. {-# INLINE [1] box #-} box :: a -> Box a box :: forall a. a -> Box a box a x = forall a. a -> Box a Box a x -- | This is the eliminator for the "stable" modality 'Box': -- -- > Γ ⊢ t :: Box 𝜏 -- > ------------------ -- > Γ ⊢ unbox t :: 𝜏 {-# INLINE [1] unbox #-} unbox :: Box a -> a unbox :: forall a. Box a -> a unbox (Box a d) = a d {-# RULES "unbox/box" forall x. unbox (box x) = x #-} {-# RULES "box/unbox" forall x. box (unbox x) = x #-}