msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Update LambdaCalculus.md

Browse Source
This commit is contained in:
Krasimir Angelov
2021-11-04 19:10:23 +01:00
committed by GitHub
parent 5342844b33
commit eaa0e55922
1 changed files with 4 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
doc/hackers-guide/LambdaCalculus.md
View File

@@ -151,7 +151,7 @@ x.s2+x.s2 where x = {s1="s"; s2="b"}
``` ```
we branch only after encountering the variant in the `s2` field. we branch only after encountering the variant in the `s2` field.
The implementation for variants requires the introduction of a nondeterministic monad with a support for logical variables. See this [paper](https://gup.ub.gu.se/file/207634): The implementation for variants requires the introduction of a nondeterministic monad with a support for mutable variables. See this [paper](https://gup.ub.gu.se/file/207634):
Claessen, Koen & Ljunglöf, Peter. (2000). Typed Logical Variables in Haskell. Electronic Notes Theoretical Computer Science. 41. 37. 10.1016/S1571-0661(05)80544-4. Claessen, Koen & Ljunglöf, Peter. (2000). Typed Logical Variables in Haskell. Electronic Notes Theoretical Computer Science. 41. 37. 10.1016/S1571-0661(05)80544-4.
@@ -161,8 +161,9 @@ newThunk :: Env s -> Term -> EvalM s (Thunk s)
newEvaluatedThunk :: Value s -> EvalM s (Thunk s) newEvaluatedThunk :: Value s -> EvalM s (Thunk s)
force :: Thunk s -> EvalM s (Value s) force :: Thunk s -> EvalM s (Value s)
msum :: [EvalM s a] -> EvalM s a msum :: [EvalM s a] -> EvalM s a
runEvalM :: (forall s . EvalM s a) -> [a]
``` ```
Here, a `Thunk` is either an unevaluated term or an already computed value. Internally, it is implement as an `STRef`. If the thunk is unevaluated, it can be forced to an evaluated state by calling `force`. In addition, `msum` makes it possible to nondeterministically branch into a list of possible actions. Here, a `Thunk` is either an unevaluated term or an already computed value. Internally, it is implement as an `STRef`. If the thunk is unevaluated, it can be forced to an evaluated state by calling `force`. Once a thunk is evaluated, it remains evaluated forever. `msum`, on the other hand, makes it possible to nondeterministically branch into a list of possible actions. Finally, `runEvalM` takes a monadic action and returns the list of all possible results.
The terms and the values in the extended language are similar with two exceptions. We add the constructor `FV` for encoding variants in the terms, and the constructors for values now take lists of thunks instead of values: The terms and the values in the extended language are similar with two exceptions. We add the constructor `FV` for encoding variants in the terms, and the constructors for values now take lists of thunks instead of values:
```Haskell ```Haskell
@@ -179,7 +180,7 @@ data Value s
| VClosure (Env s) Term -- i.e. a closure contains an environment and the term for a lambda abstraction | VClosure (Env s) Term -- i.e. a closure contains an environment and the term for a lambda abstraction
| VGen Int [Thunk s] -- i.e. an internal representation for free variables | VGen Int [Thunk s] -- i.e. an internal representation for free variables
``` ```
The eval/apply rules are similar
```Haskell ```Haskell
eval env (Vr x) args = do tnk <- lookup x env eval env (Vr x) args = do tnk <- lookup x env
v <- force tnk v <- force tnk