Skip to content

Commit

Permalink
changed comment syntax as requested
Browse files Browse the repository at this point in the history
  • Loading branch information
@dominik-muc
dominik-muc committed Dec 8, 2024
1 parent 9789161 commit 3a17029
Show file tree
Hide file tree
Showing 26 changed files with 146 additions and 147 deletions.
42 changes: 21 additions & 21 deletions examples/LWT_lexical.fram
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
(* In this example we show that lexical handlers are capable of expressing
{# In this example we show that lexical handlers are capable of expressing
lightweight threads with yield and spawn operations. The solution is not
satisfactory, but it is still interesting since it shows how our in approach
to effect capabilities we can separate an interface from an implementation
of algebraic effects. *)
of algebraic effects. #}

import List

(* We start by defining the standard State effect representing a single
{# We start by defining the standard State effect representing a single
mutable cell. Note that in Fram an effect signature is an ordinary record
of functions. A special type parameter `(effect E)` is the effect of these
effectful function, and this parameter will be automatically instantiated
Expand All @@ -16,21 +16,21 @@ import List
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
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. *)
primitive `get` and `put`, even if it is a part of the interface. #}
data State (effect E) X = State of
{ get : Unit ->[E] X
, put : X ->[E] Unit
, update : {Row} -> (X ->[E|Row] X) ->[E|Row] Unit
}

(* We declare implicit parameter named `~st`. Now, the following function may
{# 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. *)
associated effect E_st will be implicitly generalized. #}
implicit ~st {E_st} : State E_st _

(* We define get operation that works on implicit capability `~st`. It can be
{# 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
implicitly generalized). We also define similar put and update functions. *)
implicitly generalized). We also define similar put and update functions. #}
let get x =
let (State { get }) = ~st in
get x
Expand All @@ -43,11 +43,11 @@ let update f =
let (State { update }) = ~st in
update f

(* Now, we put the standard handler for state, that will become the state of the
{# Now, we put the standard handler for state, that will become the state of the
scheduler. Note that an expression that provides capability `~st` is not just
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. *)
function. All three functions becomes part of the interface. #}
handle {effect=Sched} ~st =
let get = effect x / r => fn s => r s s
let put = effect s / r => fn _ => r () s
Expand All @@ -56,13 +56,13 @@ handle {effect=Sched} ~st =
return x => fn _ => x
finally c => c []

(* Enqueue a ready thread to the scheduler queue. Note that thanks to the
{# Enqueue a ready thread to the scheduler queue. Note that thanks to the
mechanism of implicit parameters, this function uses `~st` capability, without
mentioning it explicitly. *)
mentioning it explicitly. #}
let enqueue thr =
update (fn queue => List.append queue [thr])

(* Run the scheduler. It picks one thread from the queue and runs it. *)
{# Run the scheduler. It picks one thread from the queue and runs it. #}
let sched _ =
match get () with
| [] => ()
Expand All @@ -71,29 +71,29 @@ let sched _ =
thr ()
end

(* The effect signature of lightweight threads, again as a record. We have two
{# The effect signature of lightweight threads, again as a record. We have two
operations: yield for voluntarily passing control to an another thread, and
spawn for creating new threads. The spawn function is particularly
troublesome for lexical handlers, as newly created thread should share
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. *)
but this is not possible with lexical handlers. #}
data LWT_S Row = LWT of
{ yield : Unit ->[|Row] Unit
, spawn : (Unit ->[|Row] Unit) ->[|Row] Unit
}

(* For accessing operations of LWT effect we use an another mechanism
{# For accessing operations of LWT effect we use an another mechanism
available in Fram, i.e., methods. We can associate functions with each
datatype and use usual dot syntax for accessing them. The main advantage of
methods is that the same name of the method can be used with many different
datatypes leading to a more concise and readable code. *)
datatypes leading to a more concise and readable code. #}
method yield {self = LWT {yield}} = yield
method spawn {self = LWT {spawn}} = spawn

(* Here we handle the LWT effect using pure lexical handlers. The problematic
{# 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. *)
not accessible directly via the LWT interface. #}
handle {effect=LWT} (lwt : LWT_S [LWT,IO]) =
let yield = effect _ / r => let _ = enqueue r in sched ()
let exit = effect _ / _ => sched ()
Expand All @@ -108,8 +108,8 @@ handle {effect=LWT} (lwt : LWT_S [LWT,IO]) =
in LWT { yield, spawn }
return _ => sched ()

(* Example code using LWT interface. Methods yield and spawn are accessible
via the `lwt` object. *)
{# Example code using LWT interface. Methods yield and spawn are accessible
via the `lwt` object. #}
let startThread (name : String) = lwt.spawn (fn _ =>
let _ = printStrLn (name + "1") in
let _ = lwt.yield () in
Expand Down
2 changes: 1 addition & 1 deletion examples/Modules/B/C/D.fram
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(* This import resolves to the absolute path `/Main/B/A`. *)
{# This import resolves to the absolute path `/Main/B/A`. #}
import A

pub let id = A.id
8 changes: 4 additions & 4 deletions examples/Modules/Main.fram
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(** This example serves to showcase the files-as-modules feature.
{## This example serves to showcase the files-as-modules feature.

The module hierarchy is as follows.
```
Expand All @@ -21,16 +21,16 @@
Relative imports refer to the module which is the closest to the importing
module, working upwards through the hierarchy. In this example the module
`/Main/B/C/D` imports the relative path `A`, and the nearest matching
module is `/Main/B/A`. *)
module is `/Main/B/A`. #}

import List

import A
import B/C/D as X
import /Main/B/C/D as Y (* The same import, but as an absolute path. *)
import /Main/B/C/D as Y {# The same import, but as an absolute path. #}
import B/A as A2

(* Rather than binding a module name, import the module's contents *)
{# Rather than binding a module name, import the module's contents #}
import open C

let _ =
Expand Down
98 changes: 49 additions & 49 deletions examples/Prolog.fram
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,24 @@
(* This example implements a simplified version of Prolog and serves to
illustrate the combination of implicit parameters and effect capabilities. *)
{# This example implements a simplified version of Prolog and serves to
illustrate the combination of implicit parameters and effect capabilities. #}

import List

(* Prolog terms and clauses are fairly standard. Here variables are
identified by integers and functors by strings. *)
{# Prolog terms and clauses are fairly standard. Here variables are
identified by integers and functors by strings. #}
data rec Term = TVar of Int | TFun of String, List Term

data Clause = Cl of Term, List Term

(* The signature of the standard reader effect, with a single operation
{# 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. *)
this improves readability and allows us to define methods on the type. #}
data Reader (effect E) X = Reader of (Unit ->[E] X)

(* We expose the `ask` operation of `Reader` as a method. *)
{# 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. *)
{# The standard state effect, with its accompanying methods. #}
data State (effect E) X = State of
{ get : Unit ->[E] X
, put : X ->[E] Unit
Expand All @@ -29,7 +29,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. *)
{# The standard backtracking effect. #}
data BT (effect E) = BT of
{ flip : Unit ->[E] Bool
, fail : {type X} -> Unit ->[E] X
Expand All @@ -38,8 +38,8 @@ data BT (effect E) = BT of
method flip {E, self = BT { flip } : BT E} = flip
method fail {E, self = BT { fail } : BT E} = fail

(* The method `choose` on `BT` non-deterministically selects an element
from a list. *)
{# The method `choose` on `BT` non-deterministically selects an element
from a list. #}
method choose {E, self : BT E} =
let rec choose xs =
match xs with
Expand All @@ -48,15 +48,15 @@ method choose {E, self : BT E} =
end
in choose

(* The `Fresh` effect is used to model the generation of fresh variable
identifiers in the evaluator. *)
{# 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)

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

(* ========================================================================= *)
{# ========================================================================= #}

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

(* A handler for backtracking which returns the first result wrapped in Some,
or None if no result is available. *)
{# 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|_] _) =
handle bt = BT
{ flip = effect () / r =>
Expand All @@ -80,9 +80,9 @@ let hBT (f : {effect=E} -> BT E ->[E|_] _) =
return x => Some x
in f bt

(* ========================================================================= *)
(* The following few functions on lists require a notion of equality, which is
passed as the implicit parameter `~eq`. *)
{# ========================================================================= #}
{# The following few functions on lists require a notion of equality, which is
passed as the implicit parameter `~eq`. #}

implicit ~eq

Expand All @@ -101,9 +101,9 @@ let rec assoc x xs =
| (y, v) :: xs => if ~eq x y then Some v else assoc x xs
end

(* ========================================================================= *)
(* Methods on terms and clauses that are useful for implementing variable
refreshing. *)
{# ========================================================================= #}
{# Methods on terms and clauses that are useful for implementing variable
refreshing. #}

method vars =
let ~eq (x : Int) = x.equal in
Expand Down Expand Up @@ -134,26 +134,26 @@ method rename sub =
method rename { self = Cl t ts } sub =
Cl (t.rename sub) (List.map (fn (t : Term) => t.rename sub) ts)

(* ========================================================================= *)
{# ========================================================================= #}

(* The instantiation of unification variables is represented using `State`
{# The instantiation of unification variables is represented using `State`
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. *)
the associated effect variable E_st are generalized automatically. #}
implicit ~st {E_st} : State E_st (List (Pair Int Term))

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

let setVar (x : Int) t = ~st.update (fn xs => (x, t) :: xs)

let getVar x =
let ~eq (x : Int) = x.equal in
assoc x (~st.get ())

(* The `view` method on terms can be used to view the outer-most shape of a
{# The `view` method on terms can be used to view the outer-most shape of a
term, accounting for the instantiation of unification variables.
In a realistic implementation we would keep terms that haven't been viewed
abstract to prevent accidentally pattern-matching on them. *)
abstract to prevent accidentally pattern-matching on them. #}
method rec view {self : Term} =
match self with
| TVar x =>
Expand All @@ -167,34 +167,34 @@ method rec view {self : Term} =
| TFun f ts => self
end

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

(* To further reduce verbosity, we define a function `fresh` to call the
`fresh` method of the implicit capability. *)
{# To further reduce verbosity, we define a function `fresh` to call the
`fresh` method of the implicit capability. #}
let fresh () = ~fresh.fresh ()

(* We attach additional `refresh` methods to terms and clauses, which replace
all the variables in terms with fresh unification variables. *)
{# We attach additional `refresh` methods to terms and clauses, which replace
all the variables in terms with fresh unification variables. #}

method refresh {self : Term} =
self.rename (List.map (fn x => (x, fresh ())) self.vars)

method refresh {self : Clause} =
self.rename (List.map (fn x => (x, fresh ())) self.vars)

(* ========================================================================= *)
{# ========================================================================= #}

(* Finally, we make the interpreter's knowledge base and the backtracking
{# 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. *)
effect providing a simple list of clauses. #}
implicit ~kb {E_kb} : Reader E_kb (List Clause)
implicit ~bt {E_bt} : BT E_bt

let fail () = ~bt.fail ()

(* Check whether a variable occurs in a term. *)
{# Check whether a variable occurs in a term. #}
method occurs (x : Int) =
let rec occurs (t : Term) =
match t.view with
Expand All @@ -203,7 +203,7 @@ method occurs (x : Int) =
end
in occurs self

(* Attempt to unify two terms, and signal the need to backtrack on failure. *)
{# Attempt to unify two terms, and signal the need to backtrack on failure. #}
let rec unify (t1 : Term) (t2 : Term) =
match t1.view, t2.view with
| TVar x, TVar y =>
Expand All @@ -217,24 +217,24 @@ let rec unify (t1 : Term) (t2 : Term) =
else fail ()
end

(* Retrieve some clause from the knowledge base non-deterministically. *)
{# Retrieve some clause from the knowledge base non-deterministically. #}
let kbChoose () = ~bt.choose (~kb.ask ())

(* Try to derive a term using the knowledge base. *)
{# Try to derive a term using the knowledge base. #}
let rec eval (t : Term) =
let Cl t' ts = (kbChoose ()).refresh in
let _ = unify t t' in
List.iter eval ts

(* Perform a query by substituting fresh unification variables in a term and
calling the `eval` function. *)
{# Perform a query by substituting fresh unification variables in a term and
calling the `eval` function. #}
let query (t : Term) = eval t.refresh

(* ========================================================================= *)
(* Below we finally install some handlers for the interpreter and show its
use on a simple hardcoded query. *)
{# ========================================================================= #}
{# Below we finally install some handlers for the interpreter and show its
use on a simple hardcoded query. #}

(* Example database. *)
{# Example database. #}
let kb = [Cl (TFun "f" [TVar 0, TVar 0]) []]

handle ~kb = Reader (fn () => kb)
Expand All @@ -247,7 +247,7 @@ let _ =
match
hBT (fn ~bt =>
hState [] (fn ~st =>
(* Example query. *)
{# Example query. #}
query (TFun "f" [TFun "a" [], TFun "a" []])))
with
| Some _ => printStrLn "Yes."
Expand Down
Loading

0 comments on commit 3a17029

Please sign in to comment.