gallais

open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product

variable
  m n : ℕ
  b : Bool
  Γ Δ Ξ T I O : Vec Bool n

cheery

# -*- encoding: utf-8 -*-
# Implements symmetric interaction combinators
# I took some ideas from Victor Maia's projects. 

# Bunch of cells form an interaction net.
# It's a half-edge graph.
class Cell:
    def __init__(self, kind):
        self.ports = (Port(self), Port(self), Port(self))
        self.kind = kind # 'era', 'con', 'fan'

takanuva

\/(N: *) ->
\/(z: N) ->
\/(s: N -> N) ->
N

rezoner

A spritestack model is a ZIP file with two obligatory entries:

package.json

{
    "fileType": "SpriteStackModelProject",
    "title": "Whatever"
}

coproduto

import Data.Char (isLetter, isNumber, isSpace)
import Data.List (span, dropWhile, lookup)

type ParseError = String

-- A parser is a function that takes a string and returns a parse error or a
-- pair of the parsed data and the remaining string.
type Parser a = String -> Either ParseError (a, String)

type Context = [(String, Term)]

bukzor

Type definition

T Color.
| Red.;
| Blue.;

Desugars to:

dicej

Classes
* Keith Devlin - Introduction to Mathematical Thinking - https://www.coursera.org/learn/mathematical-thinking
* Michael Genesereth - Introduction to Logic - https://www.coursera.org/learn/logic-introduction
* Robert Harper - Homotopy Type Theory - http://www.cs.cmu.edu/~rwh/courses/hott/

Books and Articles
* Benjamin C. Pierce - Types and Programming Languages - https://www.cis.upenn.edu/~bcpierce/tapl/
* x775 - Introduction to Datalog - https://x775.net/2019/03/18/Introduction-to-Datalog.html
* Bartosz Milewski - Category Theory For Programmers - https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
* Benjamin C. Pierce et al. - Software Foundations - https://softwarefoundations.cis.upenn.edu/

wrongbyte

Nested functions, closures and first-class functions

Closures store the environment along with a function. However, closures are only meaningful when a function can be excecuted from outside the scope in which it's declared.

In languages without first-class functions, you could still have nested functions, but they couldn't be used as closures, because you would not be able to execute a function outside of its original scope (since you could not assign this function to any other variable, pass it as an argument or return this function by another function).

Let's see it clearer with some examples:

function outer1() {
  const foo = 42;

hirrolot

This is the predecessor of Mazeppa.

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by th