Skip to content

Commit

Permalink
update Granule docs (auto)
Browse files Browse the repository at this point in the history
  • Loading branch information
@dorchard
dorchard committed Sep 28, 2023
1 parent 04478bc commit 2bb4e29
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions docs/modules/Primitives.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@
Com : <span class='constName'>Effect</span>
; IO : <span class='constName'>Effect</span>
; Exception : <span class='constName'>Effect</span>
; GradedFree : (labels : <span class='constName'>Type</span>) -> (<span class='constName'>Type</span> -> labels -> <span class='constName'>Type</span>) -> <span class='constName'>Effect</span></pre></div><br /><div class='code'><pre><span class='keyword'>data</span> <span class='constName'>Guarantee</span> : <span class='constName'>Type 2</span> <span class='keyword'>where</span>
; GradedFree : (labels : <span class='constName'>Type</span>) -> (<span class='constName'>Type</span> -> <span class='constName'>Set</span> labels -> <span class='constName'>Type</span>) -> <span class='constName'>Effect</span></pre></div><br /><div class='code'><pre><span class='keyword'>data</span> <span class='constName'>Guarantee</span> : <span class='constName'>Type 2</span> <span class='keyword'>where</span>
Uniqueness : <span class='constName'>Guarantee</span>
; Integrity : <span class='constName'>Guarantee</span></pre></div><br /><div class='code'><pre><span class='keyword'>data</span> <span class='constName'>Predicate</span> : <span class='constName'>Type 2</span> <span class='keyword'>where</span>
Dropable : <span class='constName'>Type</span> -> <span class='constName'>Predicate</span>
Expand Down Expand Up @@ -72,9 +72,10 @@
. a -> a [<span class='coeff'>1</span>]</pre></div><div class='desc'> Allows a linear variable to be promoted to a graded modality specifying an exact usage of 1</div><div class='code'><pre>compose : <span class='keyword'>forall</span> {a : <span class='constName'>Type</span>, b : <span class='constName'>Type</span>, c : <span class='constName'>Type</span>}
. (b -> c) -> (a -> b) -> a -> c</pre></div><div class='desc'> Linear function composition</div><a name = arithmetic><h3><a href='#' class='toplink'>[top]</a> Arithmetic</h3></a><div class='code'><pre>div : <span class='constName'>Int</span> -> <span class='constName'>Int</span> -> <span class='constName'>Int</span></pre></div><div class='desc'> Integer division</div><a name = gradedpossiblity><h3><a href='#' class='toplink'>[top]</a> Graded Possiblity</h3></a><div class='code'><pre>pure : <span class='keyword'>forall</span> {a : <span class='constName'>Type</span>}
. a -> a <<span class='eff'><span class='constName'>Pure</span></span>></pre></div><div class='desc'> Inject into a computation for any graded monad</div><div class='code'><pre>fromPure : <span class='keyword'>forall</span> {a : <span class='constName'>Type</span>}
. a <<span class='eff'><span class='constName'>Pure</span></span>> -> a</pre></div><div class='desc'> Extract form a pure computation</div><a name = algebraiceffectsandhandlers><h3><a href='#' class='toplink'>[top]</a> Algebraic effects and handlers</h3></a><div class='code'><pre>call : <span class='keyword'>forall</span> {s : <span class='constName'>Coeffect</span>, grd : s, i : <span class='constName'>Type</span>, o : <span class='constName'>Type</span>, r : <span class='constName'>Type</span>, labels : <span class='constName'>Type</span>, sigs : <span class='constName'>Type</span> -> labels -> <span class='constName'>Type</span>, e : labels}
. (i -> (o -> r) [<span class='coeff'>grd</span>] -> sigs r e) -> i -> o <<span class='eff'><span class='constName'>Eff</span> labels sigs {e}</span>></pre></div><div class='desc'> Lift a CPS-style effect operation to direct-style, also called the "generic effect" operation</div><div class='code'><pre>handle : <span class='keyword'>forall</span> {labels : <span class='constName'>Type</span>, sig : <span class='constName'>Type</span> -> labels -> <span class='constName'>Type</span>, a : <span class='constName'>Type</span>, b : <span class='constName'>Type</span>, e : <span class='constName'>Set</span> labels}
. (fmap : <span class='keyword'>forall</span> {a : <span class='constName'>Type</span>} . <span class='keyword'>forall</span> {b : <span class='constName'>Type</span>} . <span class='keyword'>forall</span> {l : labels} . (a -> b) [<span class='coeff'>0..<span class='constName'>∞</span></span>] -> sig a l -> sig b l) -> (<span class='keyword'>forall</span> {l : labels} . sig b l -> b) [<span class='coeff'>0..<span class='constName'>∞</span></span>] -> (a -> b) -> a <<span class='eff'><span class='constName'>Eff</span> labels sig e</span>> -> b</pre></div><div class='desc'> Deploy an effect handler on a computation tree</div><a name = io><h3><a href='#' class='toplink'>[top]</a> I/O</h3></a><div class='code'><pre><span class='keyword'>data</span> <span class='constName'>IOElem</span> <span class='keyword'>where</span>
. a <<span class='eff'><span class='constName'>Pure</span></span>> -> a</pre></div><div class='desc'> Extract form a pure computation</div><a name = algebraiceffectsandhandlers><h3><a href='#' class='toplink'>[top]</a> Algebraic effects and handlers</h3></a><div class='code'><pre>call : <span class='keyword'>forall</span> {s : <span class='constName'>Coeffect</span>, grd : s, i : <span class='constName'>Type</span>, o : <span class='constName'>Type</span>, r : <span class='constName'>Type</span>, labels : <span class='constName'>Type</span>, sigs : <span class='constName'>Type</span> -> <span class='constName'>Set</span> labels -> <span class='constName'>Type</span>, e : <span class='constName'>Set</span> labels}
. (i -> (o -> r) [<span class='coeff'>grd</span>] -> sigs r e) -> i -> o <<span class='eff'><span class='constName'>Eff</span> labels sigs e</span>></pre></div><div class='desc'> Lift a CPS-style effect operation to direct-style, also called the "generic effect" operation</div><div class='code'><pre>handle : <span class='keyword'>forall</span> {labels : <span class='constName'>Type</span>, sig : <span class='constName'>Type</span> -> <span class='constName'>Set</span> labels -> <span class='constName'>Type</span>, a : <span class='constName'>Type</span>, b : <span class='constName'>Type</span>, e : <span class='constName'>Set</span> labels}
. (fmap : (<span class='keyword'>forall</span> {a : <span class='constName'>Type</span>} . <span class='keyword'>forall</span> {b : <span class='constName'>Type</span>} . <span class='keyword'>forall</span> {l : <span class='constName'>Set</span> labels} . (a -> b) [<span class='coeff'>0..<span class='constName'>∞</span></span>] -> sig a l -> sig b l) [<span class='coeff'>0..<span class='constName'>∞</span></span>]) -> (<span class='keyword'>forall</span> {l : <span class='constName'>Set</span> labels} . sig b l -> b) [<span class='coeff'>0..<span class='constName'>∞</span></span>] -> (a -> b) -> a <<span class='eff'><span class='constName'>Eff</span> labels sig e</span>> -> b</pre></div><div class='desc'> Deploy an effect handler on a computation tree</div><div class='code'><pre>handleGr : <span class='keyword'>forall</span> {labels : <span class='constName'>Type</span>, sig : <span class='constName'>Type</span> -> <span class='constName'>Set</span> labels -> <span class='constName'>Type</span>, a : <span class='constName'>Type</span>, b : <span class='constName'>Set</span> labels -> <span class='constName'>Type</span>, e : <span class='constName'>Set</span> labels}
. (fmap : (<span class='keyword'>forall</span> {a : <span class='constName'>Type</span>} . <span class='keyword'>forall</span> {b : <span class='constName'>Type</span>} . <span class='keyword'>forall</span> {l : <span class='constName'>Set</span> labels} . (a -> b) [<span class='coeff'>0..<span class='constName'>∞</span></span>] -> sig a l -> sig b l) [<span class='coeff'>0..<span class='constName'>∞</span></span>]) -> <span class='keyword'>forall</span> {l : <span class='constName'>Set</span> labels} . (<span class='keyword'>forall</span> {j : <span class='constName'>Set</span> labels} . sig (b j) l -> b (j * l)) [<span class='coeff'>0..<span class='constName'>∞</span></span>] -> (a -> b {}) -> a <<span class='eff'><span class='constName'>Eff</span> labels sig e</span>> -> b e</pre></div><div class='desc'> Deploy an effect handler on a computation tree for a graded algebra</div><a name = io><h3><a href='#' class='toplink'>[top]</a> I/O</h3></a><div class='code'><pre><span class='keyword'>data</span> <span class='constName'>IOElem</span> <span class='keyword'>where</span>
Stdout
; Stdin
; Stderr
Expand Down

0 comments on commit 2bb4e29

Please sign in to comment.