In this document I wish to explain the difference between operational and denotational semantics. It may sound like a dry subject but you and I both will learn plenty from it.
Semantics of a language defines how the language behaves, where as the syntax of a programming language defines how it is formed.
| type term = | |
| | Lam of (term -> term) | |
| | Pi of term * (term -> term) | |
| | Appl of term * term | |
| | Ann of term * term | |
| | FreeVar of int | |
| | Star | |
| | Box | |
| let unfurl lvl f = f (FreeVar lvl) |
| (** Core Types *) | |
| module Syntax = | |
| struct | |
| type t = | |
| | Local of int | |
| | Hole of string | |
| | Let of string * t * t | |
| | Lam of string * t | |
| | Ap of t * t | |
| | Pair of t * t |
On September 28, 2021, I asked on Twitter:
PL Twitter:
you get to recommend one published PL paper for an undergrad to read with oversight by someone experienced. the paper should be interesting, approachable, and (mostly) self-contained.
what paper do you recommend?
| #!/bin/bash | |
| # Colors definitions | |
| RED='\033[0;31m' | |
| GREEN='\033[0;32m' | |
| NC='\033[0m' # No Color | |
| BOLD=$(tput bold) | |
| NORMAL=$(tput sgr0) | |
| # Check if necessary applications are installed |
| #!/usr/bin/awk -f | |
| # This program is a copy of guff, a plot device. https://github.com/silentbicycle/guff | |
| # My copy here is written in awk instead of C, has no compelling benefit. | |
| # Public domain. @thingskatedid | |
| # Run as awk -v x=xyz ... or env variables for stuff? | |
| # Assumptions: the data is evenly spaced along the x-axis | |
| # TODO: moving average |
Rust error handling is nice but obligatory. Which makes it sometimes plenty of code.
Functions return values of type Result that is "enumeration". In Rust enumeration means complex value that has alternatives and that alternative is shown with a tag.
Result is defined as Ok or Err. The definition is generic, and both alternatives have
| -- https://gist.github.com/ChristopherKing42/d8c9fde0869ec5c8feae71714e069214 | |
| -- https://github.com/MaiaVictor/Cedille-Core/blob/master/old_haskell_implementation/Core.hs | |
| -- https://crypto.stanford.edu/~blynn/lambda/pts.html | |
| module Other where | |
| import Prelude hiding (pi, succ) | |
| import Control.Monad.Reader |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE StandaloneDeriving #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| module Typed where | |
| import Prelude hiding (Left, Right, fst, snd) | |
| data Elem as a where |
