GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-24 02:12:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

Update LambdaCalculus.md

Browse Source
This commit is contained in:
Krasimir Angelov
2021-11-04 16:42:23 +01:00
committed by GitHub
parent 86dfebd925
commit 6fc3a2177c
1 changed files with 15 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -13,17 +13,17 @@ In the rest of we will discuss the implementation of the partial evaluator.
We will start with the simplest possible subset of the GF language, also known as simple lambda calculus. It is defined as an algebraic data type in Haskell, as follows: We will start with the simplest possible subset of the GF language, also known as simple lambda calculus. It is defined as an algebraic data type in Haskell, as follows:
```Haskell ```Haskell
data Term data Term
= Vr Ident -- e.g. variables: x,y,z ... = Vr Ident -- i.e. variables: x,y,z ...
| Cn Ident -- e.g. constructors: cons, nil, etc. | Cn Ident -- i.e. constructors: cons, nil, etc.
| App Term Term -- e.g. function application: @f x@ | App Term Term -- i.e. function application: @f x@
| Abs Ident Term -- e.g. \x -> t | Abs Ident Term -- i.e. \x -> t
``` ```
The result from the evaluation of a GF term is either a constructor applied to a list of other values, or an unapplied lambda abstraction: The result from the evaluation of a GF term is either a constructor applied to a list of other values, or an unapplied lambda abstraction:
```Haskell ```Haskell
type Env = [(Ident,Value)] type Env = [(Ident,Value)]
data Value data Value
= VApp Ident [Value] -- e.g. constructor application = VApp Ident [Value] -- i.e. constructor application
| VClosure Env Term -- e.g. a closure contains an environment and the term for a lambda abstraction | VClosure Env Term -- i.e. a closure contains an environment and the term for a lambda abstraction
| VGen Int [Value] -- we will also need that special kind of value for the partial evaluator | VGen Int [Value] -- we will also need that special kind of value for the partial evaluator
``` ```
For the lambda abstractions we build a closure which preserves the environment as it was when we encountered the abstraction. That is necessary since its body may contain free variables whose values are defined in the environment. For the lambda abstractions we build a closure which preserves the environment as it was when we encountered the abstraction. That is necessary since its body may contain free variables whose values are defined in the environment.
@@ -159,17 +159,17 @@ The monad (let's call it `EvalM`) must provide the primitives:
```Haskell ```Haskell
data Term data Term
= Vr Ident -- e.g. variables: x,y,z ... = Vr Ident -- i.e. variables: x,y,z ...
| Cn Ident -- e.g. constructors: cons, nil, etc. | Cn Ident -- i.e. constructors: cons, nil, etc.
| App Term Term -- e.g. function application: @f x@ | App Term Term -- i.e. function application: @f x@
| Abs Ident Term -- e.g. \x -> t | Abs Ident Term -- i.e. \x -> t
| FV [Term] -- e.g. a list of variants: t1|t2|t3|... | FV [Term] -- i.e. a list of variants: t1|t2|t3|...
type Env s = [(Ident,Thunk s)] type Env s = [(Ident,Thunk s)]
data Value s data Value s
= VApp Ident [Thunk s] -- e.g. constructor application = VApp Ident [Thunk s] -- i.e. constructor application
| VClosure (Env s) Term -- e.g. 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] -- e.g. an internal representation for free variables | VGen Int [Thunk s] -- i.e. an internal representation for free variables
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