michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of github.com:pepijnkokke/sf

Browse source 
* 'master' of github.com:pepijnkokke/sf:
  updated stlc
This commit is contained in:
Pepijn Kokke 2017-03-10 16:03:16 +00:00
commit f682a4c8d7
No known key found for this signature in database
GPG key ID: EF467CD387487CB8
1 changed files with 4 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Stlc.lagda
View file

@ -8,7 +8,6 @@ permalink : /Stlc
module Stlc where module Stlc where
\end{code} \end{code}
<div class="hidden">
\begin{code} \begin{code}
open import Maps using (Id; id; _≟_; PartialMap; module PartialMap) open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
open import Data.Empty using (⊥; ⊥-elim) open import Data.Empty using (⊥; ⊥-elim)
@ -19,7 +18,6 @@ open import Function using (_∘_; _$_)
open import Relation.Nullary using (Dec; yes; no) open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
\end{code} \end{code}
</div>
# The Simply Typed Lambda-Calculus # The Simply Typed Lambda-Calculus
@ -161,13 +159,9 @@ so we will STLC's function type as `_⇒_`.
data Type : Set where data Type : Set where
bool : Type bool : Type
_⇒_ : Type → Type → Type _⇒_ : Type → Type → Type
\end{code}
<div class="hidden">
\begin{code}
infixr 5 _⇒_ infixr 5 _⇒_
\end{code} \end{code}
</div>
### Terms ### Terms
@ -194,21 +188,20 @@ to Agda (and other functional languages like ML, Haskell, etc.),
which use _type inference_ to fill in missing annotations. We're which use _type inference_ to fill in missing annotations. We're
not considering type inference here. not considering type inference here.
Some examples... We introduce $$x, y, z$$ as names for variables. The pragmas ensure
that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
\begin{code} \begin{code}
x = id 0 x = id 0
y = id 1 y = id 1
z = id 2 z = id 2
\end{code}
<div class="hidden">
\begin{code}
{-# DISPLAY id zero = x #-} {-# DISPLAY id zero = x #-}
{-# DISPLAY id (suc zero) = y #-} {-# DISPLAY id (suc zero) = y #-}
{-# DISPLAY id (suc (suc zero)) = z #-} {-# DISPLAY id (suc (suc zero)) = z #-}
\end{code} \end{code}
</div>
Some examples...
$$\text{idB} = \lambda x:bool. x$$. $$\text{idB} = \lambda x:bool. x$$.