You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Apr 1, 2025. It is now read-only.
-- NB: We derive the 'Semigroup' instance for 'Concrete' to take the second argument. This is equivalent to stating that the return value of an imperative sequence of statements is the value of its final statement.
Copy file name to clipboardExpand all lines: semantic-core/src/Analysis/Eval.hs
+3Lines changed: 3 additions & 0 deletions
Original file line number
Diff line number
Diff line change
@@ -43,6 +43,9 @@ eval Analysis{..} eval = \case
43
43
addr <- alloc n
44
44
v <- bind n addr (eval (instantiate1 (pure n) b))
45
45
v <$ assign addr v
46
+
-- NB: Combining the results of the evaluations allows us to model effects in abstract domains. This in turn means that we can define an abstract domain modelling the types-and-effects of computations by means of a 'Semigroup' instance which takes the type of its second operand and the union of both operands’ effects.
47
+
--
48
+
-- It’s also worth noting that we use a semigroup instead of a semilattice because the lattice structure of our abstract domains is instead modelled by nondeterminism effects used by some of them.
Copy file name to clipboardExpand all lines: semantic-core/src/Analysis/Typecheck.hs
+2Lines changed: 2 additions & 0 deletions
Original file line number
Diff line number
Diff line change
@@ -49,6 +49,8 @@ data Monotype f a
49
49
typeType=TermMonotypeMeta
50
50
51
51
-- FIXME: Union the effects/annotations on the operands.
52
+
53
+
--| We derive the 'Semigroup' instance for types to take the second argument. This is equivalent to stating that the type of an imperative sequence of statements is the type of its final statement.
Copy file name to clipboardExpand all lines: semantic-core/src/Control/Monad/Module.hs
+19Lines changed: 19 additions & 0 deletions
Original file line number
Diff line number
Diff line change
@@ -8,6 +8,25 @@ module Control.Monad.Module
8
8
9
9
importControl.Effect.Carrier
10
10
11
+
--| Modules over monads allow lifting of a monad’s product (i.e. 'Control.Monad.join') into another structure composed with the monad. A right-module @f m@ over a monad @m@ therefore allows one to extend @m@’s '>>=' operation to values of @f m@ using the '>>=*' operator.
12
+
--
13
+
-- In practical terms, this means that we can describe syntax which cannot itself bind or be substituted for variables, but which can be substituted inside when containing a substitutable expression monad. For example, we might not want to allow variables in a declaration context, but might still want to be able to substitute for e.g. globally-bound variables inside declarations; a 'RightModule' instance expresses this relationship nicely.
14
+
--
15
+
-- Note that we are calling this a right-module following Maciej Piróg, Nicolas Wu, & Jeremy Gibbons in _Modules Over Monads and their Algebras_; confusingly, other sources refer to this as a left-module.
16
+
--
17
+
-- Laws:
18
+
--
19
+
-- Right-identity:
20
+
--
21
+
-- @
22
+
-- m >>=* return = m
23
+
-- @
24
+
--
25
+
-- Associativity:
26
+
--
27
+
-- @
28
+
-- m >>=* (k >=> h) = (m >>=* k) >>=* h
29
+
-- @
11
30
class (forallg.Functorg=>Functor (fg), HFunctorf) =>RightModulefwhere
Copy file name to clipboardExpand all lines: semantic-core/src/Data/Scope.hs
+19-7Lines changed: 19 additions & 7 deletions
Original file line number
Diff line number
Diff line change
@@ -12,8 +12,8 @@ module Data.Scope
12
12
, instantiate1
13
13
, instantiate
14
14
, instantiateEither
15
-
, un
16
-
, unEither
15
+
, unprefix
16
+
, unprefixEither
17
17
) where
18
18
19
19
importControl.Applicative (liftA2)
@@ -110,11 +110,23 @@ instantiateEither :: Monad f => (Either a b -> f c) -> Scope a f b -> f c
110
110
instantiateEither f = unScope >=> incr (f .Left) (>>= f .Right)
111
111
112
112
113
-
un:: (Int->t->Maybe (a, t)) ->t-> (Stacka, t)
114
-
un from = unEither (matchMaybe . from)
115
-
116
-
unEither:: (Int->t->Either (a, t) b) ->t-> (Stacka, b)
117
-
unEither from = go (0::Int) Nil
113
+
--| Unwrap a (possibly-empty) prefix of @a@s wrapping a @t@ using a helper function.
114
+
--
115
+
-- This allows us to peel a prefix of syntax, typically binders, off of a term, returning a stack of prefixing values (e.g. variables) and the outermost subterm rejected by the function.
116
+
unprefix
117
+
:: (Int->t->Maybe (a, t)) --^ A function taking the 0-based index into the prefix & the current term, and optionally returning a pair of the prefixing value and the inner subterm.
118
+
->t--^ The initial term.
119
+
-> (Stacka, t) --^ A stack of prefixing values & the final subterm.
120
+
unprefix from = unprefixEither (matchMaybe . from)
121
+
122
+
--| Unwrap a (possibly-empty) prefix of @a@s wrapping a @b@ within a @t@ using a helper function.
123
+
--
124
+
-- Compared to 'unprefix', this allows the helper function to extract inner terms of a different type, for example when @t@ is a right @b@-module.
125
+
unprefixEither
126
+
:: (Int->t->Either (a, t) b) --^ A function taking the 0-based index into the prefix & the current term, and returning either a pair of the prefixing value and the next inner subterm of type @t@, or the final inner subterm of type @b@.
127
+
->t--^ The initial term.
128
+
-> (Stacka, b) --^ A stack of prefixing values & the final subterm.
0 commit comments