Skip to content

Commit

Permalink
Update the parser, Raw and Desugar
Browse files Browse the repository at this point in the history
The parser is updated to match the new version of Surface. Miscellanous
syntax changes requested in existing issues or discussed elsewhere were
made too:
* #156 method definitions no longer treat self in a special way, but
  the tests were not updated;
* #173;
* effect variable naming near the `handle` construct uses `/`;
* no more rows and `effect` or `label` fields (but the keyword `label`
  still cannot be used as an identifier).

The tests and examples should mostly parse now, though not necessarily
as expected due to the changes to method definitions.
  • Loading branch information
forell committed Jan 9, 2025
1 parent e630aef commit a29e86b
Show file tree
Hide file tree
Showing 36 changed files with 453 additions and 442 deletions.
19 changes: 10 additions & 9 deletions examples/LWT_lexical.fram
Original file line number Diff line number Diff line change
Expand Up @@ -14,19 +14,20 @@ import List
an additional function `update`. Implementing such an update function in
some other languages with algebraic effects might turn out to be
troublesome, as a handler of `update f` should call function `f` at the call
site of `update`, where potentially more effects (described by `Row`) are
site of `update`, where potentially more effects (described by `F`) are
available. In Fram, update function can be implemented on top of more
primitive `get` and `put`, even if it is a part of the interface. #}
data State (effect E) X = State of
data State E X = State of
{ get : Unit ->[E] X
, put : X ->[E] Unit
, update : {Row} -> (X ->[E|Row] X) ->[E|Row] Unit
, update : {F} -> (X ->[E,F] X) ->[E,F] Unit
}

{# We declare implicit parameter named `~st`. Now, the following function may
use `~st` as a regular variable. In such a case, `~st` together with the
associated effect E_st will be implicitly generalized. #}
implicit ~st {E_st} : State E_st _
parameter E_st
parameter ~st : State E_st _

{# We define get operation that works on implicit capability `~st`. It can be
used in any context, where a variable named ~st is available (or can be
Expand All @@ -48,7 +49,7 @@ let update f =
a value, but more complex series of let-expressions. First, we define
standard get and put operations, and then on top of them we define the update
function. All three functions becomes part of the interface. #}
handle {effect=Sched} ~st =
handle ~st =
let get = effect x / r => fn s => r s s
let put = effect s / r => fn _ => r () s
let update f = put (f (get ())) in
Expand Down Expand Up @@ -78,9 +79,9 @@ let sched _ =
the handler with the parent thread without sharing parent's continuation.
With dynamic handlers we can just create a new handler for the same effect,
but this is not possible with lexical handlers. #}
data LWT_S Row = LWT of
{ yield : Unit ->[|Row] Unit
, spawn : (Unit ->[|Row] Unit) ->[|Row] Unit
data LWT_S E = LWT of
{ yield : Unit ->[E] Unit
, spawn : (Unit ->[E] Unit) ->[E] Unit
}

{# For accessing operations of LWT effect we use an another mechanism
Expand All @@ -94,7 +95,7 @@ method spawn {self = LWT {spawn}} = spawn
{# Here we handle the LWT effect using pure lexical handlers. The problematic
spawn operation is implemented via more primitive fork and exit functions,
not accessible directly via the LWT interface. #}
handle {effect=LWT} (lwt : LWT_S [LWT,IO]) =
handle (lwt : LWT_S [LWT,IO]) / LWT =
let yield = effect _ / r => let _ = enqueue r in sched ()
let exit = effect _ / _ => sched ()
let fork = effect _ / r =>
Expand Down
30 changes: 17 additions & 13 deletions examples/Prolog.fram
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,15 @@ data Clause = Cl of Term, List Term

{# The signature of the standard reader effect, with a single operation
used to obtain a value of type X. While we do not need to wrap functions
`{effect=E} -> Unit ->[E] X` in a data type to use them as capabilities,
this improves readability and allows us to define methods on the type. #}
data Reader (effect E) X = Reader of (Unit ->[E] X)
`{E} -> Unit ->[E] X` in a data type to use them as capabilities, this
improves readability and allows us to define methods on the type. #}
data Reader E X = Reader of (Unit ->[E] X)

{# We expose the `ask` operation of `Reader` as a method. #}
method ask {E, self = Reader ask : Reader E _} = ask

{# The standard state effect, with its accompanying methods. #}
data State (effect E) X = State of
data State E X = State of
{ get : Unit ->[E] X
, put : X ->[E] Unit
}
Expand All @@ -30,7 +30,7 @@ method put {E, self = State { put } : State E _} = put
method update {E, self : State E _} f = self.put (f (self.get ()))

{# The standard backtracking effect. #}
data BT (effect E) = BT of
data BT E = BT of
{ flip : Unit ->[E] Bool
, fail : {type X} -> Unit ->[E] X
}
Expand All @@ -50,14 +50,14 @@ method choose {E, self : BT E} =

{# The `Fresh` effect is used to model the generation of fresh variable
identifiers in the evaluator. #}
data Fresh (effect E) X = Fresh of (Unit ->[E] X)
data Fresh E X = Fresh of (Unit ->[E] X)

method fresh {E, self = Fresh fresh : Fresh E _} = fresh

{# ========================================================================= #}

{# The standard state handler, defined as a higher order function. #}
let hState init (f : {effect=E} -> State E _ ->[E|_] _) =
let hState init (f : {E} -> State E _ ->[E,_] _) =
handle st = State
{ get = effect () / r => fn s => r s s
, put = effect s / r => fn _ => r () s
Expand All @@ -68,7 +68,7 @@ let hState init (f : {effect=E} -> State E _ ->[E|_] _) =

{# A handler for backtracking which returns the first result wrapped in Some,
or None if no result is available. #}
let hBT (f : {effect=E} -> BT E ->[E|_] _) =
let hBT (f : {E} -> BT E ->[E,_] _) =
handle bt = BT
{ flip = effect () / r =>
match r True with
Expand All @@ -84,7 +84,7 @@ let hBT (f : {effect=E} -> BT E ->[E|_] _) =
{# The following few functions on lists require a notion of equality, which is
passed as the implicit parameter `~eq`. #}

implicit ~eq
parameter ~eq

let rec nub xs =
match xs with
Expand Down Expand Up @@ -140,7 +140,8 @@ method rename { self = Cl t ts } sub =
containing an association list of instantiations. As this effect is pervasive
throughout our implementation, we declare it as an implicit, so that it and
the associated effect variable E_st are generalized automatically. #}
implicit ~st {E_st} : State E_st (List (Pair Int Term))
parameter E_st
parameter ~st : State E_st (List (Pair Int Term))

{# We also define a pair of functions that let us modify and read `~st`. #}

Expand Down Expand Up @@ -169,7 +170,8 @@ method rec view {self : Term} =

{# As with `~st`, the capability to generate fresh identifiers ~fresh is also
declared implicit. #}
implicit ~fresh {E_fresh} : Fresh E_fresh Int
parameter E_fresh
parameter ~fresh : Fresh E_fresh Int

{# To further reduce verbosity, we define a function `fresh` to call the
`fresh` method of the implicit capability. #}
Expand All @@ -189,8 +191,10 @@ method refresh {self : Clause} =
{# Finally, we make the interpreter's knowledge base and the backtracking
capability implicit as well. The knowledge base is represented as a reader
effect providing a simple list of clauses. #}
implicit ~kb {E_kb} : Reader E_kb (List Clause)
implicit ~bt {E_bt} : BT E_bt
parameter E_kb
parameter ~kb : Reader E_kb (List Clause)
parameter E_bt
parameter ~bt : BT E_bt

let fail () = ~bt.fail ()

Expand Down
10 changes: 5 additions & 5 deletions examples/Pythagorean.fram
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import List
data Triples = Triple of Int, Int, Int

{# The standard backtracking effect. #}
data BT (effect E) = BT of
data BT E = BT of
{ flip : Unit ->[E] Bool
, fail : {type X} -> Unit ->[E] X
}
Expand All @@ -31,11 +31,11 @@ method triples {E, self : BT E} (n : Int) =
if a * a + b * b == c * c then Triple a b c
else self.fail ()


implicit ~bt {E_bt} : BT E_bt
parameter E_bt
parameter ~bt : BT E_bt

{# The function `takeFirst` returns the first triple found. #}
let takeFirst (f : {effect=E} -> BT E -> Int ->[E|_] _) (n: Int) =
let takeFirst (f : {E} -> BT E -> Int ->[E,_] _) (n: Int) =
handle bt = BT { flip = effect () / r =>
match r True with
| None => r False
Expand All @@ -47,7 +47,7 @@ let takeFirst (f : {effect=E} -> BT E -> Int ->[E|_] _) (n: Int) =
in f bt n

{# The function `takeAll` returns list of all triples found. #}
let takeAll (f : {effect=E} -> BT E -> Int ->[E|_] _) (n: Int) =
let takeAll (f : {E} -> BT E -> Int ->[E,_] _) (n: Int) =
handle bt = BT
{ flip = effect () / r => List.append (r True) (r False)
, fail = effect () => []
Expand Down
2 changes: 1 addition & 1 deletion examples/Tick.fram
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@

import List

let count (f : {type E} -> (_ ->[|E] _) ->[|E] _) g =
let count (f : {type E} -> (_ ->[E] _) ->[E] _) g =
handle tick = effect _ / k => fn (n : Int) => k () (n + 1)
return _ => fn n => n
finally c => c 0
Expand Down
4 changes: 2 additions & 2 deletions lib/Prelude.fram
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,11 @@ pub let not b = if b then False else True

pub let charListToStr = (extern dbl_chrListToStr : List Char -> String)

pub let chr {~re : {type X} -> Unit ->[|_] X} (n : Int) =
pub let chr {~onError : Unit ->[_] Char} (n : Int) =
if n >= 0 && n < 256 then
(extern dbl_intToChr : Int -> Char) n
else
~re ()
~onError ()

pub let printStrLn = extern dbl_printStrLn : String ->[IO] Unit
pub let printStr = extern dbl_printStr : String ->[IO] Unit
Expand Down
Loading

0 comments on commit a29e86b

Please sign in to comment.