Sketch of PL-1 programming language

Not to be confused with IBM PL/I¹.

1Goals

The goal of PL-1 is to be a comprehensive system modeling language and programming language. By "comprehensive", we mean taking into account all components of the system, including application, database, and infrastructure, and taking into account all processes of the system, including development, maintenance, and deployment.

(Is that goal too big?)

2Milestone planning?

Version, milestone, man-day

• 0.0.0: Capture essential complexity
  • Type definitions
  • Use-case expression language / feature expression language, something like ML?
• 0.1.0
  • Translation to Java 8, Servlet API 3.1, HTML 5, CSS 3, JDBC 4.2, PostgreSQL 9.5.
• 0.2.0
  • HTTP basic authentication
  • Authorization
  • Sign out
• 0.3.0
  • Query parallelization and caching
  • Implement some of https://en.wikipedia.org/wiki/Relational_algebra
  • Query cost guesser
• 0.4.0
  • Google OAuth.

Unplanned:

• Read-only storage
• Writable storage

3Prior arts

Should we just use the Mozart/Oz language?²³⁴

The Racket language?

4Pure expression evaluation

The meaning of a pure expression does not depend its evaluation order (reduction strategy).

But, what about \( (\lambda x y . x) ~ 2 ~ \frac{1}{0} \)? Is that expression pure? It reduces to 2 in normal-order, but it reduces to bottom in applicative-order. The answer is: we should not even talk about reducing that expression because it is ill-typed: the type of division should have been Number → Number → Maybe Number because division has a side-effect: exceptions and non-terminations are side-effects; bottom is a side-effect. Therefore a division expression is not a pure expression.

5Object-property system

An object has zero or more properties. Mutable.

6GUI programming

Listeners eventually produce spaghetti code in big GUI applications; the interaction logic is all over the place.

What is prone to modification in a GUI application? The appearance? The behavior?

Explicit actions: undo-redo requires that actions be reified.

Explicit actions ameliorate listeners?

Event buses reduce the number of connections (compared to star / direct-point-to-point connection) from quadratic to linear.

Functional reactive programming (FRP) does not obviate explicit actions for undo-redo.

7Idea: Explicit evaluation

The meaning of (define X Y) is: If the prefix of the current expression matches X, then replace that prefix with Y.

The expression (normalize E) reduces to the value that results from beta-normalizing the expression E.

The expression (apply-normal (lambda Param Body) Arg) reduces to Body with each bound occurrence of Param replaced with Arg. (Should Param/Arg be shared or not?)

The expression (apply-strict (lambda Param Body) Arg) evaluates Arg to Val and reduces to Body with each bound occurrence of Param replaced with Val.

Should the evaluation strategy be attached to apply or lambda or both?

If it is both, then should the outer annotation override the inner annotation, or the other way around?

(apply-normal (lambda Param Body) Arg)
;; or
(apply (lambda-normal Param Body) Arg)

;; Here apply's strategy overrides lambda's strategy.
(apply-strict (lambda-normal Param Body) Arg)

;; The default strategy should be adjustable,
;; but should the default-strategy-setting be lexically scoped or dynamically scoped?
(apply (lambda Param Body) Arg)

The current expression is initially (main).

;; rewrite
(define (f x y) (+ x y))
(define (g x y) (normalize (+ x y)))
(define (h x y) (normalize-head (+ x y)))

Alternative: explicit delay and force.

8Designing the implementation

The implementation is probably an interpreter.

8.1Implementation requirements

The interpreter must be ready to accept user input in less than 500 ms since the user starts the interpreter on a typical 2019 machine.

It is also important to have fast build if there is a build step.

8.2Sketch

I am thinking of building the interpreter on top of Racket or Scheme or Lisp or Prolog.

8.3Ideas and reading list

Perhaps the easiest way to make a programming language is to extend lambda calculus?

The easiest extension is some constants.

How do we let the programmers choose the reduction strategy?

1982 A consistent extension of the lambda-calculus as a base for functional programming languages https://www.sciencedirect.com/science/article/pii/S0019995882904582

8.4Embed lambda calculus

(What is this? Design and implementation.)

I think I'll begin by sketching a lambda-calculus interpreter in Racket.

Suppose that we want to write an interpreter for language G (guest) in language H (host).

H = Host (Racket)

G = Guest (lambda calculus)

An example of an HVal is a Racket integer?.

A GVal is the host representation of a guest value.

normalize : GExp → GVal reduce : GExp → GExp interpret : GExp → HVal wrap : GVal → HVal unwrap : HVal → GVal

unwrap . wrap = id

unwrap . normalize = interpret

normalize = normalize . reduce

The reader should produce a syntax object, not just a datum, because we want errors to report locations.

I think it is unfortunate in Scheme/Racket that read ignores comments. I think read should produce a #%comment node for a comment. That is, there should be a variant of read that reads concrete-syntax-tree nodes and not abstract-syntax-tree nodes.

9Maintainability?

Related topics:

• interactive programming
• inspectability, traceability, debuggability
• serialization, state restoration
• reverse-engineerability. documentability, literate programming

10Interactive programming, serialization, and state restoration

Like some Lisp/Smalltalk images, save/dump and restore/resume.

Is it wise to change some parts of the program that the machine is running, like changing the wheels while the car is running?

Terms: interactive programming, online programming (may be confused with Web editor?)

10.1Why have state restoration?

State restoration is for interactive programming.

Also for packaging and distributing stand-alone applications, as in Prolog and Racket.

10.2Naïvely restoring states causes security problems

State restoration can be abused to break encapsulation by modifying the internal state of an object.

State restoration must be designed to be secure against all cases in which the attacker fully controls the dump and can tell the program to restore arbitrarily but in which the attacker does not have access to the binary/source/OS-running-process address space, that is, in which the attacker cannot attach a debugger.

Or we tell users to only restore from dumps they themselves created.

But we let users do it anyway. If we make a wrench, it is not our responsibility if the user chooses to hit his own head with it; he is free to hurt himself; but we share some blame if he chooses to hit others' heads with it. If we dislike those consequences, we should not make a wrench.

(Ramble.)

A technology not only solves problems but also creates its own problems.

(End ramble.)

10.3Storing graphs without naming conflicts

The problem with #0# is that the string representation cannot be naïvely concatenated? (Can it?)

With local binding like lambda, the string representation can be naïvely concatenated.

Cyclic data are much prettier in non-strict languages.

(named a (cons 1 a))
;; or
(μ a (cons 1 a))
;; represents
a = (cons 1 a) = (1 1 1 ...)

(Compare: fixed point operator, μ-regular expressions)

The meaning of \( \mu x . y \) is the \( z \) that is \( y \) but with all bound occurrence of \( x \) replaced with \( z \). By "bound", we mean that \( \mu \) binds the same way \( \lambda \) does.

\( \mu x . y \) can be thought of as (named x y) where every bound occurrence of x in y refers to (is the name of) the entire expression (named x y) itself.

That is, \( \mu x . y = fix (\lambda x . y) \) where fix is a fixed-point combinator⁵ (fix(f) = f(fix(f))).

10.4For interactive programming, all states must be serializable

All states must be serializable (dumpable and restorable).

Each global variable should declare how to initialize and snapshot itself.

11Threading

The programmer should be able to choose between cooperative and preemptive multithreading, but the default should be preemptive.

12Binding

The syntax tree is enriched with location and binding information.

Then, bindings are computed.

A bound name = local name + definition site (the original name and where it is defined).

compute-bindings : Cst-Node → Bound-Cst-Node

To determine whether two names refer to the same referent, use referent=?. This is similar to Scheme's unfortunately named free-identifier=?.

• determine whether two names refer to the same thing
• get definition site (get where a name is defined)

Question: Should the binding information also include types, for overloading (ad-hoc polymorphism)? Do we want overloading?

13Macros

Macros are replaced with explicit program transformations?

Scheme's magic ellipsis comes from Kohlbecker & Wand 1987 [5]⁶⁷. [4]⁸.

Scheme macros are call-by-name; Scheme procedures are call-by-value.

Perhaps macros should be replaced with explicit evaluation; perhaps the language should enable the programmer to choose evaluation strategies such as normal-order and applicative-order.

14Namespaces

I want namespaces to be first-class, that is, a value, that can be manipulated like other values, that can be named by define, like integers, strings, etc.

In principle, a namespace can be represented by a lambda that maps a name to its meaning.

Necessary operations:

• namespace-lookup: Look-up an exported name in a namespace.
• namespace-list-exports: List the names exported by a namespace.
• namespace-exports?: Determine whether a name is exported by a namespace.

More operations?

• namespace-imports: Analyze the imports of a namespace?

14.1Naïve lambda representation of namespaces

For example:

;;  A namespace expression form

(namespace
  (import ns1 [a b c])
  (export [num inc])
  (define num (+ a b))
  (define (inc x) (+ x 1)))

;;  translates to a plain lambda form

(lambda (name)
  ;; (import ns1 [a b c])
  (define a (ns1 'a))
  (define b (ns1 'b))
  (define c (ns1 'c))
  ;; internal definitions
  (define num (+ a b))
  (define (inc x) (+ x 1))
  ;; (export [num inc])
  (case name
    [(num) num]
    [(inc) inc]
    [($imports) '( (ns1 [a b c]) )]
    [($exports) '(x inc)]
    [else (error)]))

We rely on partial evaluation to inline namespace access such as (ns 'inc).

Problem: I worry that partial evaluation may increase compilation time too much.

Problem: Perhaps $imports and $exports should be placed out of band (not mixed with the symbols exported by the namespace). Also, perhaps imports and exports should be opaque structs. But then we have to resort to Scheme structs.

15Documentation system

Comments are first-class in the sense that read does not discard comments; it is just that comments are interpreted as no-operations and may be discarded by compilation.

($comment "This strange code exists because ...")

Problem: I don't want to repeat the name.

($doc foo "The var.")
(define foo 1)

(define (fun)
  ($doc "The function.")
  1)

Literate programming?

16Modules

Loading/requiring a file or module should not have any side effects. Like Haskell. Unlike Scheme, Racket, Prolog.

Racket tips:

Avoid side-effects in modules

It is evil to have side-effects when loading modules.

Instead, it is better to make a module that exports a mutable struct.

racket/gui is particularly evil: it cannot be required in different phases in the same OS process. But that is because the underlying wxWidgets is evil (global variables).

17Proper tail calls, and continuations

If you want to implement proper tail calls, you may as well implement continuations?

They complicate implementation and analysis? Or do they simplify?

They don't interact nicely with other language features? They have difficult corner cases?

Why do we want continuations? What benefit does it bring that justifies its cost?

Continuations enable us to give meaning to imperative control constructs using denotational semantics which were commonly used to give meaning to functional programs? [7]⁹

But is that good enough?

18Multi-processing and isolation?

If you have a C program that has global variables, and you need to run two instances of it, then you may run two OS processes from the same binary, if the program does not write any files.

Can a program have no absolute file system paths?

19Example fragment?

This is similar to, if not inspired by, Moseley & Marks 2006 [6].

The essence of data is what can be done with it, not what it is? Only database designers care about how data is stored. Database users care about what can be done with the data in a reasonable amount of time.

Balzer 1967 [1]?

The goal is to come up with an expressive enough specification language whose specifications happen to be translatable to reasonably efficient implementations. The goal is to make a specification language whose denotational semantics nicely coincide with its operational semantics. The goal is to make a specification language that happens to also be a programming language.

Is that Coq or Agda? Program extraction?

type surrogate_id = natural;

let employee = type {
    id : surrogate_id;
    name : string;
    birth_date : date;
    join_date : date;
    payments : collection payment;
};

let payment = type {
    id : surrogate_id;
    date : date;
    amount : real;
    note : string;
};

let department = type {
    id : surrogate_id;
    name : string;
    establishment_date : date;
};

let my_app_ = application {
    -- application state type
    state = {
        employees : relation employee;
        departments : relation department;
    };
    -- An use case is an application-state endofunction.
    add_employee (e : employee) (s : state) : state =
        ASSERT e IN s.employees
};

let my_app_imp = implementation of my_app with state mapping {
    employees -> db, schema "my_app", table "employees";
    departments -> db, schema "my_app", table "employees";
} with type replacement {
    surrogate_id -> uint64; -- with overflow check, non modular
} where
    db = database {
        type = postgresql;
        host = 127.0.0.1;
        username = "user";
        password = "pass";
    };

let f (x : natural) = x + 1

let g = quotient of f by replacing natural arithmetic with modular unsigned 32-bit arithmetic
let h = quotient of f by replacing natural arithmetic with overflow-checked unsigned 32-bit arithmetic

20Design

The language is embedded in Prolog.

There is some type-checking.

Our goals:

• The key concept: Move accidental complexity from the source language to the translator.
• Specify system state (application + database).
• Specify use cases and business logic.
• Generate a Java program and a PostgreSQL database implementing the specification.

What is XL¹⁰?

21Kernel/core language

The core language is intended for machines. Humans should use the convenient language.

Each expression carries its own type.

Combine lambda calculus and relational calculus/algebra.

Should we use relational algebra or relational calculus¹¹? Codd's theorem¹² says that they are equivalent. Relational model¹³? Codd prefers relational calculus¹⁴? What is a relational database?¹⁵

21.1Lambda calculus

lambda(Param,Body) is a lambda expression.

let(Binds,Body). Example: let([ a = 1, b = 2 ], a + b)

apply(Fun,Arg)

21.2Basic expressions

set(Type,List) represents a set in which each element has type Type.

function(Dom,Cod,Map) function expression. Example: function([1,2],natural,[1-10,2-20]). Example: function(natural,natural,lambda([x],x+1)). The function must be total; it must be defined for each element of the domain.

21.3Relation expressions

A relation expression describes a relation (a triple of domain, codomain, and mapping).

relation(Dom,Cod,Map). Example: relation(natural,natural,[1-10, 2-20, 3-30]).

all(Dom,Cod,S) where S is a storage expression

Example: relation(natural,natural,lambda([x],(x+1 ; x+2))). Nondeterministic lambda.

How do we have anonymous predicates? Fixed points? Clojure recur?

21.4Storage expressions

A storage expression describes how data is stored.

Storage expressions:

memory: volatile memory, destroyed when the program terminates.

postgresql(Props). Example: postgresql([major(9), minor(5), host(Host), port(Port), catalog(bar), schema(foo), table(bar)])

21.5Implementation expressions

A function may be implemented as a dictionary, a lookup table, a subroutine, or something else.

21.6Types

A value may have several types.

A type describes a set of values.

Name types.

atom describes Prolog atoms

term describes Prolog terms, which is everything expressible in Prolog

expression describes our language expressions

Numeric types.

natural

integer

rational

real

Mathematical types.

singleton(Value) describes a singleton set that contains only Value

set(Type) describes a homogeneous set

relation(Dom,Cod)

function(Dom,Cod)

field(Name,Type) where Name is an atom

sequence(Types) where Types is a list of Type

A Record is a sequence of Fields.

product(Types) where Types is a list of Type

union(Types) where Types is a list of Type

Questionable types.

identifier(Bit) is unique only inside the same system instance

int(Bit)

uint(Bit)

thing

string

21.7Should we adopt Lisp syntax?

(relation natural natural
  (lambda (x) (choice (+ x 1) (+ x 2))))

(function (1 2) natural ((1 10) (2 20)))

22Convenience language

22.1Expressions

function(Map) finite function expression, with domain and codomain inferred to be the smallest possible that encompasses the mapping. Example: function([1-a, 2-b, 3-c]).

23Concepts?

23.1What program, execution, and termination mean in declarative paradigms

In functional paradigm:

• The program is a big lambda expression.
• Execution is beta-reduction / term-rewriting.
• Execution terminates when the program reaches normal form (is no longer beta-reducible).

In satisfying-logic paradigm:

• The program is a big logic formula.
• Execution is trying to satisfy the formula.
• Execution terminates when satisfiability is determined.

In theorem-proving paradigm:

• The program is a big logic formula, presumably in conjunctive-normal form.
• Execution is trying to prove the main(world) goal.
• Execution terminates when the goal is proved or disproved.

23.2Records, also for namespaces and modules

We want records because records obviate namespaces and modules.

We want namespaces and modules because they are necessary for humans to manage large programs.

23.2.1We don't want to represent records as functions.

We can describe the semantics of a record r as a function r : string -> expression.

There are several options to pretty-print a record:

• Define a show-record function that is different from show.
• But we want polymorphic show. We want one show function to work for all things.
• If a record is represented by a lambda abstraction, then pretty-printing the record will pretty-print a lambda abstraction. We don't want that. We want pretty-printed records to look like how we write records.

23.2.2We want records to be applicable like lambda; we add a new beta-reduction rule for "applying" records.

Record access is function application. To get the field fld or record rec, evaluate rec fld.

The record rec with the the field fld updated to new is the expression \ name -> IF name = fld THEN new ELSE rec fld.

We add this beta-reduction rule:

• If X is a record, and Y is a string, then X Y reduces to get X Y.

We want to pretend that records are functions. We want to use records as if they were functions. But we don't want records to be functions; we want to pretty-print records as records, not as lambda abstractions.

23.2.3Modules as record functions

A module is a function taking a record and giving a record. The input is called imports or dependencies. The output is called exports.

Example:

\ { add; } -> { add_one: \ x -> add x 1; }

23.2.4Record expressions

We add these expression syntax rules:

• If each of x1,…,xn is a label and each of e1,…,en is an expression, then {x1:e1; ...; xn:en;} is a record expression.
• union R S is a record union expression.
• record update expression (should be polymorphic)
• record filtering/selection/intersection expression

An example of a record expression is {id: \ x -> x; app: \ f x -> f x;}.

23.2.5Labels

A label is a string. If the label doesn't contain funny characters, it doesn't have to be quoted. For example, {"a":1;} and {a:1;} are the same thing.

Should we generalize label to expression?

23.3Modeling all data

23.3.1Hypothesis: data = ADTs + records + row polymorphism

Hypothesis: All data can be modeled by a combination of these:

• product (tuple)
• sum (alternative, union)
• record (tuple with named components)
• row polymorphism

Can we use web standards to define an ontology (so we can use Protege to edit it)? https://protege.stanford.edu/

• Does Eclipse EMF have textual representation?

23.3.2Church-representation of products, sums, and algebraic data types in general

https://en.wikipedia.org/wiki/Lambda_calculus#Pairs

Let [x] mean the representation of x.

A product (a,b) can be represented as [(a,b)] = \ f -> f [a] [b].

The left projection p1 is represented as [p1] = \ p -> p (\ a b -> a).

If we assume the sum type A + B, then:

• The choice inl a can be represented as [inl a] = \ f g -> f [a].
• The choice inr b can be represented as [inr b] = \ f g -> g [b].

A recursive data type such as "stream a = (a, stream a)" can be represented as:

• [cons h t] = \ f -> f [h] [t].

Thus [a : b : c : …] = \ f -> f [a] (\ f -> f [b] (\ f -> f [c] …)).

A recursive data type such as "list a = nil | cons a (list a)" can be represented as:

• [nil] = \ f g -> f.
• [cons x y] = \ f g -> g [x] [y].

Natural numbers "nat = z | s nat":

• [z] = \ f g -> f.
• [s x] = \ f g -> g [x].

Thus:

• [s z] = \ f g -> g (\ f g -> f)

23.3.3Reverse semantics

Semantics maps syntax to mathematical object.

Reverse semantics maps mathematical object to syntax. Reverse semantics is representation. Reverse semantics is realization.

Example of reverse semantics is representing the tuple (x,y) with the lambda abstraction \ f -> f [x] [y] where [x] denotes the representation of x.

https://en.wikipedia.org/wiki/Realizability

23.3.4Self-interpreter

1994 article "Efficient Self-Interpretation in Lambda Calculus"

23.4Representing knowledge; logic programming; symbolic AI

• https://en.wikipedia.org/wiki/Logic_programming#Knowledge_representation
• https://en.wikipedia.org/wiki/Knowledge_representation_and_reasoning

Example: We encode "a todo item has an int64 id" as

IF entity todo_app todo E THEN property E int64 id.

23.5Dynamic binding, contextual holes

• 1996 article "Enriching the lambda calculus with contexts: toward a theory of incremental program construction" https://dl.acm.org/citation.cfm?id=232652
• 1998 article "A lambda-calculus for dynamic binding" https://core.ac.uk/download/pdf/82810390.pdf
• 1998 article "Computing with Contexts: A simple approach" https://core.ac.uk/download/pdf/82065430.pdf
• 2009 article "Two-level Lambda-calculus" https://www.sciencedirect.com/science/article/pii/S1571066109002400

23.6Interpreters: Giving different meanings to the same syntax

Sometimes we want to interpret the same syntax (appearance, source code, text) differently.

23.7Precise memory accounting

We want precise memory accounting to enable the runtime to limit memory usage.

23.8Execution state reification, save states, saving and loading states, pausing and resuming computations

We want execution state reification so that we can do live process migration.

23.9After-2018 programming language requirements

23.9.1Ergonomic error handling

23.9.2REPL (read-eval-print loop)

The language must not preclude making a REPL for it.

REPL is important for immediate feedback, experimentation, exploration, and playing around.

23.9.3Example of mixing nominal and structural subtyping

https://www.eclipse.org/n4js/features/nominal-and-structural-typing.html

23.9.4Programming language should separate modeling and binding. Can we combine dynamic binding and static typing?

Example of binding is import statement.

23.9.5Paradigm, approach, viewpoint, worldview?

• graph programming languages

  • https://cstheory.stackexchange.com/questions/3906/what-are-theoretically-sound-programming-languages-for-graph-problems

    • https://www.cs.york.ac.uk/plasma/wiki/index.php?title=GP_%28Graph_Programs%29
    • 2007, PhD thesis, Steinert, "The graph programming language GP"

    • a short visual example of "conditional rule schemata"

      • 2010, article, "Hoare Logic for Graph Programs"
    • https://markorodriguez.com/2013/01/09/on-graph-computing/

    • https://en.wikipedia.org/wiki/Gremlin_(programming_language)

• equational programming?

  • 2017-2018, https://www.cs.vu.nl/~tcs/ep/

  • term-rewriting

    • retired, Q language

      • http://q-lang.sourceforge.net/examples.html

      • superseded by Pure

        • https://agraef.github.io/pure-lang/
        • https://en.wikipedia.org/wiki/Pure_(programming_language)
        • https://github.com/agraef/pure-lang/wiki/Rewriting

    • Joy

• 2002, article, "Stochastic Lambda Calculus and Monads of Probability Distributions"
• "Purely functional lazy nondeterministic programming", paywall

• relational programming (pure logic programming?)

  • miniKanren

    • Byrd PhD thesis https://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf

      • mentions other programming languages: Prolog, Mercury, Curry
• https://en.wikipedia.org/wiki/Multi-adjoint_logic_programming

• ramble

  • https://www.researchgate.net/project/Ontology-oriented-programming
  • http://www.doc.ic.ac.uk/~klc/OntProg.html

23.9.6Low-code? Programming for the masses?

Limited programming?

What can we assume about the user's skill/knowledge/background?

• https://en.wikipedia.org/wiki/End-user_development
• https://en.wikipedia.org/wiki/Low-code_development_platforms

23.10Toward a language with first-class syntax?

• composable grammars?

  • 2013, article, Viera & Swierstra, "First Class Syntax, Semantics, and Their Composition" http://www.cs.ru.nl/P.Achten/IFL2013/symposium_proceedings_IFL2013/ifl2013_submission_21.pdf

    • 2013, PhD thesis, Viera, "First Class Syntax, Semantics, and Their Composition" file:///home/erik/Downloads/viera.pdf
  • 1990, "A Primer for Program Composition Notation"
  • https://stackoverflow.com/questions/953185/composable-grammars
  • OMeta

  • Programming languages with programmable syntax

    • Katahdin

  • parsing expression grammar, packrat

    • "Parsing ought to be easier"

      • https://news.ycombinator.com/item?id=2330830

        • "PEGs are one class of cleanly composable grammars."?
  • http://www.cs.cmu.edu/~Compose/

  • cryptographic protocol analysis

    • https://en.wikipedia.org/wiki/Universal_composability

• Programming languages with macros

  • Common Lisp
  • Scheme
  • Kotlin?
  • Clojure?
  • Scala? https://www.scala-lang.org/blog/2017/11/27/macros.html

23.11Enabling metaprogramming

• metaprogramming - Why is ML called Meta-Language? - Stack Overflow

• related?

  • https://github.com/PostgREST/postgrest
  • http://rosecompiler.org/

• Metaprogramming

  • http://kaitai.io/

    • from description, generate parsers for binary data (as opposed to text data)

• Aspect-oriented programming is a restricted form of metaprogramming.

  • relationship between Aspect-Oriented Programming and Functional Programming

    • 2009, article, "What Does Aspect-Oriented Programming Mean for Functional Programmers?", pdf
    • 2008, article, "On Feature Orientation and Functional Programming", pdf

    • 2016, article, "Realtime collaborative editor. Algebraic properties of the problem.", html

      • see also Darcs patch theory
    • 2008, PhD thesis, "An Integrated System to Manage Crosscutting Concerns in Source Code", pdf

    • 2003, article, "Language-independent aspect-oriented programming", pdf available

• Java metaprogramming

  • Similar products

    • libraries

      • INRIA Spoon
      • The javax.lang.model package of the Java standard library, but it does not model method bodies.

    • environments

      • Eclipse Modeling Framework (EMF)
      • JetBrains MPS (Meta Programming System)
      • Stratego/XT
      • TXL
      • Eclipse Xtext and Eclipse Xtend

    • programming languages

      • Eclipse Xtend

    • parser generators

      • WP:Compiler-compiler
      • WP:Comparison of parser generators
      • ANTLR (Another Tool for Language Recognition)
      • JavaCC
      • YACC, Bison; with Lex, Flex

  • Related concepts

    • Model-driven development
    • Model-driven architecture

23.12Automatic (program) differentiation

• What is the relationship between incremental lambda-calculus and automatic differentiation of programs (or of algebraic data types)?

23.13Extending functions

Not only classes, but also functions, should be extensible.

"To extend the function \( f : A \to B \) to the function \( f' : A' \to B' \)" means:

• For every \( x \in A \), we have \( f(x) = f'(x) \).
• \( A \subseteq A' \).
• \( B \subseteq B' \).

A consequence: Every occurrence of \( f \) can be replaced with \( f' \) while preserving the meaning of the containing expression.

23.14A sketch about reusable language-oriented programming: CommonMark, Liquid, and Jekyll, reusable grammar?

I want something like this:

data CommonMark = ... -- CommonMark AST
data Liquid = ... -- Liquid AST
type Jekyll = CommonMark + Liquid

parse_cm : String -> Parser CommonMark
parse_lq : String -> Parser Liquid
parse_jk : String -> Parser Jekyll
parse_jk = parse_cm + parse_lq

• design - Composable Grammars - Stack Overflow
• Grammar reuse
• melt-umn/silver: An attribute grammar-based programming language for composable language extensions
• OMeta, Katahdin

23.15Whole-program optimization?

• https://stackoverflow.com/questions/3416980/why-arent-whole-program-optimizations-more-prevalent-now/27757382

23.16TODO <2018-09-15> Make the programming language

• [3]
• [2]

23.17TODO <2018-09-15> Find out how type systems may guarantee pointer safety

Is escape analysis the only way?

23.17.1TODO <2018-09-15> Study Sixten type system

23.17.2TODO <2018-09-15> Study Rust type system

See Rust type system reference.

23.18Combine things and let the programmer choose?

23.18.1Combine nominal subtyping and structural subtyping

23.19Effects?

• Reddit post "Try/Catch and Async/Await are just a specialized form of Algebraic Effects!" https://www.reddit.com/r/ProgrammingLanguages/comments/9kzcz6/trycatch_and_asyncawait_are_just_a_specialized/
  • 2016 article "Algebraic Effects for Functional Programming" https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/algeff-tr-2016-v2.pdf
    • "we show how algebraic effects generalize over common constructs like exception handling, state, iterators and async-await"
  • <2018-10-08> not yet performant

23.20Abdullah research roadmap

• Abbreviations:

  • CCC: Cartesian closed category (Wikipedia)

• Abdullah wants to make a monad-aware programming language.

  • Categories enable us to organize a hierarchy of effects?

    • effectful over category \( C \) = extends category \( C \)?

• The plan is to research two related things in parallel:

  • using algebraic subtyping to mix parametric subtyping and inheritance subtyping

    • Stephen Dolan's Ph.D. thesis "Algebraic subtyping"

      • "Type systems which support subtyping care about the direction of data flow."
      • "Find the simplest algebra of types, and some syntax for them"
    • Wikipedia: Subtyping

    • Scala already tries to join parametric subtyping and inheritance subtyping. What is the problem with Scala?

• Related: functional programming research.

• Who is Abdullah?

  • Abdullah a.k.a. Kim-Ee Yeoh is atamo.com.

23.20.1Research questions

1. Possible questions

   • What is the result of CPS-transforming a recursive function?

   fac 0 = 1
   fac n = n * fac (n - 1)
   
   fac 0 k = k 1
   fac n k = fac (n - 1) $ \ x -> k (n * x)

   Conjecture: Every recursive function can be transformed to a tail-recursive function with a helper function \( f(x) = f(g(x)) \).

   fac 0 = 1
   fac n = n * fac (n - 1)
   
   fach (a, 0) = (a, 0)
   fach (a, n) = fach (a * n, n - 1)
   
   fac n = fach (1, n)

   How do we enable the caller to step the recursion?

   fac n = \ k -> k (\ x -> x * fac (n - 1) k) n
   fac n (\ f x -> f x)
   
   tri 0 = 0
   tri n = n + tri (n - 1)
   
   tri :: Nat -> ((x -> c -> Nat) -> Nat -> Nat)
   tri 0 = \ k -> 0
   tri n = \ k -> k (\ x c -> x + tri (n - 1) c) n
   
   inc x = inc (x + 1)
   
   inc x = \ k -> k (\ ) (x + 1)

   • github: dorchard/unfix: Takes a recursive function and syntactically unties the recursive knot

2. What is the relationship between self-reference, recursion, and fixed points?

   We say that \( x \) is a fixed point of \( f \) iff \( f(x) = x \).

   MO 126513: categories of recursive functions

   • What is the essence of self-recursion?

     • fix does not exist in a strict language.

       • "The Z combinator will work in strict languages […]" WP: Fixed-point combinator

         • The Z combinator is obtained by eta-expanding the Y combinator.

3. What is the formal definition of strict, non-strict, eager, and lazy?

   The difference is explained by luqui on SO 7140978. - Strict and non-strict are about meaning (denotational semantics?). Eager and lazy are about operation (operational semantics?). - Strictness is a domain-theoretic concept. Laziness is a computer implementation detail. - This uses Haskell to introduce domain theory: Wikibooks: Haskell: Denotational semantics. - In Haskell, the least fixed point operator can be defined as fix f = f (fix f). - Why is bottom the least fixed point of id? Every \( x \) is a fixed point of an identity function \( x \mapsto x \), isn't it? - What is the ordering? - "Semantic approximation order" - Haskell wiki is wrong? It conflates non-strictness with normal-order reduction strategy? - A simple example of denotational semantics using a language of binary numerals - WP: Binary combinatory logic. Its semantics is SK calculus (SKI calculus without the redundant I combinator) which is equivalent to lambda calculus. - we can execute non-strict functions eagerly, for example by strictness analysis or speculative execution.

   People are often sloppy with these terms. Redditors. Experts. Researchers. Academics. It is true that Haskell is non-strict. It is true that Haskell (as implemented by GHC) is lazy.

   We can infer these formal definitions: - A function \( f \) is strict iff \( f(\bot) = \bot \). - "a strict function must map bottom to bottom" (from the SO answer)

4. How do we represent general recursion by a monad? How do we add general recursion to TFP? How do we do it with monads?

   Here we try to salvage [McBride2015].

   TODO write the problem: how McBride's General doesn't compose

   • Is McBride's General really a monad?
   • Is Abdullah's M really a monad?
   • Did Abdullah mistranslate McBride's General?
   • Is there a way to transform begin-step-end to McBride's General or Abdullah's M?
   • Start with axioms, then infer the data types.

   These are the axioms that we want M to satisfy. - rec f . rec g = rec (ext f . g) - rec f . rec g = rec (f <=< g) - rec pure = id

   How do we translate a recursive function f : a -> b to an explicitly recursive function f : a -> m b?

   -- Abdullah's M, obtained by translating
   -- the General in [McBride2015] from Agda to Haskell
   data M s t a
       = Em a
       | Ap (t -> M s t a) s
   
   cata :: (a -> r) -> ((t -> r) -> s -> r) -> r
   cata ar xrxr m = fix $ \ self m -> case m of
       Em a -> ar a
       Ap xma x -> xrxr (self . xma) x

   • Why do we want to add general recursion to TFP?

     • Adding general recursion to a TFPL makes programming in that language more practical.

   • There are several attempts to add general recursion to TFP.

     • [Nordstrom1988] (terminating general recursion)
     • [Bove2001] (simple general recursion in type theory)
     • [Capretta2005] (general recursion via coinductive types)
     • [McBride2015] (Turing-completeness totally free)
     • me on 2018-04-07? "Approximating general recursion in TFP"?
     • A non-termination monad inspired by domain theory, part of the documentation of Coq's GeneralRec library

   • How are monads useful in FP?

     • Monads allow embedding a strict language in a lazy language [Wadler1996].
     • "Monads may be regarded as a mild generalization of continuation-passing style." [Wadler1996]
   • Philip Wadler's research on monads

   • Reading triage:

     • Moggi 1991: Notions of computation and monads

       • Programs should form a category.

         • Every type becomes an object in the category.
         • Every (one-parameter) function becomes a morphism in the category.
       • "Kleisli triples are just an alternative description for monads. Although the former are easy to justify from a computational perspective, the latter are more widely used in the literature on category theory and have the advantage of being defined only in terms of functors and natural transformations, which make them more suitable for abstract manipulation."
       • Moggi's most cited paper, according to Google Scholar

       • Moggi's home page

         • Moggi's list of his publications

           • recent paper: 2010 "Monad Transformers as Monoid Transformers". Theoretical Computer Science, TCS vol.411
     • Moggi 1989: Computational lambda-calculus and monads
     • 2017 Uustalu Partiality and container monads
     • [Sheard2003] (a pure language with default strict evaluation order and explicit laziness)
     • [Wadler1998] (how to add laziness to a strict language without even being odd)
     • [Wadler1992] "explores the use of monads to structure functional programs"
     • Monad for lazy evaluation, Scheme, SRFI-40 mail archive, Andre van Tonder
     • Not all computational effects are monads

     • 2018 Tomas Petricek What we talk about when we talk about monads

23.20.2Result of meeting on 2018-04-21

• https://mvanier.livejournal.com/2897.html
• Applicative Functor is a homomorphism over CCC (Cartesian closed category)?

• We can use a category as the denotation of a functional programming language.

  • An example of a category:

    • One object: Unit
    • One morphism:

    • Two functions:

      • f0 x = Unit
      • f1 x = x

• What is a CCC? It is a category that satisfies the axioms in WP: CCC.

23.20.3Agenda for 2018-04-21

1. Totality is not about termination

   Consider this example. This recursion is not structural. However, it terminates under normal-order beta-reduction strategy.

   -- Constant function.
   f : Nat -> Nat
   f _ = 0
   
   main : Nat
   main = f main

   Is main a total function? Does that question make sense? Note that main is not a mathematical function. The denotation of main might be a mathematical function.

   Does totality depend on the reduction strategy? Does that question make sense?

   I conjecture that every general recursive function can be transformed into its begin-step-end form. See "Approximating general recursion in TFP".

2. I think we can't add a Lazy Monad instance to Strict Haskell without changing the language semantics

   Here I try to (and fail to) add a Lazy monad to an imaginary language Strict Haskell (SH).

   Imagine SH, a language with Haskell syntax but with Scheme's applicative-order beta reduction (AOBR) instead of Haskell's normal-order beta reduction. AOBR means: to evaluate f x, first evaluate x, and then evaluate f x. SH is strict, and Haskell is lazy.

   An inhabitant of the type Lazy a can be thought of as a thunk that will return an inhabitant of a.

   To construct an expression of type Lazy a, combine these: - The expression bottom constructs a thunk will fail. - The expression pure x constructs a thunk that will return x. Note that x is evaluated before the thunk is constructed. - The expression delay f constructs a thunk that will return the result of evaluating f Unit. The type of f is Unit -> a. Note that f unit is not evaluated when the thunk is constructed, unlike pure. - The expression eval t evaluates or forces the thunk t. The type of eval is Lazy a -> Maybe a.

   We want to embed laziness into SH. Formally, this means that we want this equation to hold

   eval (bottom >>= \ x -> pure c) = Just c
   

   but this is impossible in SH because the >>= is strict.

   However, if the type of >>= were this

   (Monad m) => m (Lazy a) -> (Lazy a -> m (Lazy b)) -> m (Lazy b)
   

   then it would be possible to embed laziness into SH.

   Thus Lazy cannot be a Monad instance in SH.

   Monads allow embedding a strict language in a lazy language [Wadler1996]. We are trying the reverse (embedding a lazy language in a strict language). We have just tried the most naive way. It failed.

3. Does TFP really sacrifice Turing-completeness?

   • What is a rigorous definition of Turing-completeness?

     • Wikipedia: "a system of data-manipulation rules (such as a computer's instruction set, a programming language, or a cellular automaton) is said to be Turing complete or computationally universal if it can be used to simulate any Turing machine"

       • What does "simulate" mean?

     • What is the relationship among total Turing machine, partial Turing machine, total function, and partial function? See Wikipedia: Machine that always halts.

   • Why do you ask this?

     • We've been thinking that totality precludes Turing-completeness, but Conor McBride disagrees in [McBride2015].

23.20.4Results

1. Is continuation the mother of all monads?

   Abdullah wants to prove that continuation is the mother of all monads.

   I think I have a partial proof of that for all Haskell-98 type endofunctions.

   The folder abdullah-conjecture contains a proposed partial proof of the Abdullah conjecture for all Haskell 98 type endofunctions. The proof can be checked by the Lean theorem prover version 3. See also the Lean prover home page. To edit Lean source files, use Visual Studio Code and its Lean plugin.

23.20.5Reading triage

1995, D. A. Turner, Elementary Strong Functional Programming

Godel's System T revisited

Total Functional Programming in a Partial Impure Language

Type theory and functional programming: Can we see type theory as a functional programming language?

Thierry Coquand page at Chalmers

MO 126513: Categories of recursive functions

Denotational semantics and rewrite rules for FP: "We consider languages whose operational semantics is given by a set of rewrite rules."

allisons.org: Denotational Semantics

The Y-combinator is \( \lambda f. (\lambda x. f ~ (x ~ x)) ~ (\lambda x. f ~ (x ~ x)) \). WP: Fixed-point combinator

Simple Denotational Semantics for the Lambda Calculus, Pω Revisited?

23.20.6Undigested information fragments

• "Partiality is an effect" https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf
• "Partiality Monad Transformer" https://stackoverflow.com/questions/15192897/partiality-monad-transformer
• http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.pdf

• categorical programming language

  • http://web.sfc.keio.ac.jp/~hagino/thesis.pdf
  • https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory
  • https://softwareengineering.stackexchange.com/questions/216635/category-theory-based-language
• "Kleisli triple over a category"
• "Category formed by the Kleisli triples over a category"

• Moggi 1991:

  • "Kleisli triples are just an alternative description for monads. Although the former are easy to justify from a computational perspective, the latter are more widely used in the literature on category theory and have the advantage of being defined only in terms of functors and natural transformations, which make them more suitable for abstract manipulation."
• Where does monad come from? Who invented it? Why was it invented?
• What is the relationship among monad, natural transformation, Kleisli category of a monad, Eilenberg-Moore what, adjunction?
• Has some semantics link http://math.andrej.com/2016/08/06/hask-is-not-a-category/comment-page-1/
• 2010, "Subtyping, Declaratively: An Exercise in Mixed Induction and Coinduction", Nils Anders Danielsson and Thorsten Altenkirch

23.21Language design

• https://github.com/mjambon/ocaml-wishlist

23.22Designing configuration languages

23.22.1What is a configuration language?

Configuration language is programming language minus Turing-completeness.

23.22.2What is the best configuration language?

2018-08-31: Dhall is the pinnacle of configuration languages, in my opinion, as far as I know.

Can a configuration language get any better than Dhall?

How far can we push configuration languages without Turing-completing it?

Dhall isn't the only Turing-incomplete language. There are also Coq, Lean, Agda, and others. Can we use these as configuration languages? Should we?

23.22.3Some rants

Write your configuration in Dhall. You minimize duplication. It generates YAML/JSON.

Why stop there? Replace all your YAML, JSON, XML, INI, PROPERTIES, configurations with Dhall.

2018-08-31: We're considering HashiCorp Terraform. I think they should use Dhall, or at least learn from Dhall, instead of creating their own HCL (HashiCorp Configuration Language). We have a "Terraform Workaround Engineer" here at work.

Someone has done that: dhall-terraform.

23.23Designing markup languages

A markup language adds some semantics to text.

• Finding the best document typesetting/processing system

  • What are some markup languages?

    • http://www.nongnu.org/skribilo/
    • markdown
    • reST (restructured text)
    • TeX, LaTeX
    • Unix roff, troff, nroff, man, GNU groff
    • GNU info

• Finding a lightweight semantic markup language with fixed ontology

  • WP:Lightweight markup language

  • Which markup language?

    • reST
    • Textile. GitHub Pages stopped supporting this.
    • S-expression
    • not Markdown?
    • https://tiddlywiki.com/static/WikiText.html
    • https://hackage.haskell.org/package/mmark

    • Org mode for Emacs – Your Life in Plain Text

      • Using Markdown instead of Org Mode – Jack Baty – Medium

  • Which tool?

    • pandoc
    • hakyll

  • Which editor?

    • Vim
    • Emacs
    • Visual Studio Code

    • Too experimental

      • clearly.pl reminds me of TiddlyWiki.

23.24Class-based programming

• What is a class?

  • What is a class?

    • A class is a blueprint (a template).
    • A class is a way of organizing your program.

  • What does a class have?

    • A class has name, fields, and methods.

  • What does a class do?

    • A class groups data and code that needs that data.
• Every object belongs to a class.

• In class-based programming:

  • Objects don't have methods.
  • Classes have instance methods.
  • Each instance method can be called with an instance as a hidden argument.

• From procedural point of view, these two are the same:

// Java

object.method(arg0, arg1, ...)

// C

method(object, arg0, arg1, ...)

• The dot is just a syntax for passing an implicit first argument.
• The dot operator associates to the left:

a.b().c().d() = ((a.b()).c()).d()

23.25Intersection between programming language search and software engineering: The effect of programming language on software quality

• https://developers.slashdot.org/story/14/11/05/0530228/the-effect-of-programming-language-on-software-quality
  • 2014 article "A Large Scale Study of Programming Languages and Code Quality in Github" pdf
    • I don't know enough to determine whether the methodology is valid.

23.26Beginning programming language research

• A practitioner's guide to reading programming languages papers
  • from top scoring links : ProgrammingLanguages
• https://waleedkhan.name/blog/getting-a-job-in-pl/
  • https://www.reddit.com/r/ProgrammingLanguages/comments/9ffiky/how_to_get_a_job_in_programming_languages/

23.27Racket syntax objects, read-syntax; does Prolog/Haskell have this?

• Must understand: reader and expander.
  • Racket parsing has two stages/levels: reader and expander.
  • (My guess?) The output of the reader is the input of the expander?
• https://docs.racket-lang.org/guide/hash-reader.html
  • "The difference between read and read-syntax is that read is meant to be used for data while read-syntax is meant to be used to parse programs."
  • Readtables work at the reader level.
  • Macros work at the expander level.
    • Macros can't change the lexicon.

23.28Stop abusing the equals sign

The equals sign should be used for equations only and nothing else.

Consider this fragment in a hypothetical functional programming language.

hang : Nat
hang = hang

The fragment hang = hang falsely suggests that it is an equation like \(x = x\). We can substitute \(x\) with any natural number, and the equation \(x = x\) will still hold. But that is not what we mean with hang. We are defining a rewrite rule, not an equation. Thus we should write hang => hang instead.

In an equation, the left and right side are equal. We don't care if they are flipped. In a rewrite rule, we care about direction. We want to start with \(1 + 1\) and end with \(2\), not the other way, unless we are writing a theorem prover.

Programming is hard enough already. Let's not make it harder for students. Stop using confusing notation.

Reading triage:

• Misuse of the equals sign: An entrenched practice from early primary years to tertiary mathematics

23.29Problems that the language has to solve

23.29.1Solving the expression problem

23.29.2Solving the AST decoration problem / AST typing problem

• Other names of this problem:
  • AST typing problem
  • "Trees that grow" problem
• common problem in parsing: how to decorate AST in a functional language
  • 2013, article, The AST typing problem, Edward Z. Yang
    • 2010, discussion, "The AST typing problem", LTU
  • Embracing the Any type
    • JavaParser added an Object data field to the AST Node base class, but they changed their minds.
      • https://github.com/javaparser/javaparser/issues/456
      • https://github.com/javaparser/javaparser/pull/472
  • Structural typing
    • TypeScript (JavaScript) is ideal for AST decoration problem? You just add a key to the AST node object you want to decorate.
      • Any language with structural typing is ideal?

      interface Node {
      }
      
      interface Node_parse extends Node {
      }
      
      interface Node_desugar extends Node_parse {
      }
      

  • Loosely-typed Haskell?
    • This is basically the JavaScript way.

    type Key = String
    data Value
        = VNum Double
        | VStr String
        | VObj Object
    type Object = [(Key, Value)]
    type Node = Object

  • 2017, article, "Trees that grow", https://www.microsoft.com/en-us/research/uploads/prod/2016/11/trees-that-grow.pdf
    • "The compiler writer is then faced with two unpalatable choices. She can define a new data type representing the output decorated tree, at the cost of much duplication. Or she can write a single data type with all the necessary fields and constructors, at the cost of having many unused fields and constructors at different stages of compilation."
    • However, we can fake extensible ADTs with pattern synonyms, with Fix, and without type families.
      • Similar endeavors
        • https://wiki.haskell.org/Type_composition
      • Haskell doesn't beta-reduce types.
      • This is an example code:

      data Exp_ name exp
          = Var name
          | Add exp exp
          | ...
      
      data Locd a
          = MkLocd Loc a
      
      data Typed t a = MkTyped t a
      
      newtype Compose f g a = MkCompose { unCompose :: f (g a) }
      
      type PsExp name = Fix (Compose Locd (Exp_ name))
      type TcExp name = Fix (Compose Locd (Compose Typed (Exp_ name)))
      
      -- To ameliorate the verbosity:
      
      class Exp name exp where
          var :: name -> exp
          add :: exp -> exp -> exp
          ...
      
      instance Exp (PsExp name) where ...
      instance Exp (TcExp name) where ...

  • What if GHC can "inline" data types at compile time? What if GHC can "inline" A and B in data A = MA Int; data B = MB Int String; data E = EA A | EB B;, producing data E = EA Int | EB Int String? Implementing this with Haskell 98 types should be straightforward.
  • related - "Data types a la carte" - http://hackage.haskell.org/package/compdata - Haskell type composition - https://wiki.haskell.org/Extensible_datatypes
• Other people's efforts
  • https://brianmckenna.org/blog/type_annotation_cofree
• https://discuss.ocaml.org/t/is-it-feasible-to-write-parsers-without-using-polymorphic-variants-for-ast-representation/1906

1. Other solutions to the AST typing problem / trees-that-grow problem; using recursion schemes for separation of concern in functional programming

   • "Program Reduction: A Win for Recursion Schemes" http://www.newartisans.com/2018/04/win-for-recursion-schemes/
     • Annotated expression trees
       • "The first moment when this recursion scheme went from an interesting idea to a good design decision was when someone created an issue on GitHub, asking to add location information to the expression tree."
     • Abstract Definitional Interpreters?
       • 2017 article "Abstracting Definitional Interpreters" https://arxiv.org/abs/1707.04755
     • boilerplate
     • recommends using recursion schemes

   That is an interesting idea, but some important questions remain:

   • How do we do that without boilerplate (for the library writer)?
   • How do we do that without performance penalty?

23.30object = lambda + record + mutation?

let self = {
        prop = 1;
        foo = \ () -> self.prop + 1;
}; in self

23.31Logic programming with explicit side-effects with force-predicate

The meaning of force(X) is that force(X) succeeds iff it has changed the world such that X will succeed after force(X) returns. Thus the interpreter has to check for race conditions? Is this requirement too difficult?

?- file_content('foo', A). -- unify A with the contents of file 'foo'

?- force(file_content('foo', [1,2,3])). -- replace the content of file 'foo' with [1,2,3]

23.32Prolog as a term-rewriting meta-interpreter

The Prolog rule "A :- B" can be interpreted in two ways. The first is the well-known proof-theoretic interpretation "to prove A, prove B". The second is the rewriting-system interpretation "rewrite A to B".

23.33Functions as semantics of lambda calculus?

Key idea: A lambda abstraction is not a function, but a function can be the semantics of a lambda abstraction.

A semantic of a lambda abstraction is a function, that is, a triple \((A,B,M)\) where \(A\) is the domain, \(B\) is the codomain, and \(M\) is the mapping.

What is the semantic of \( \lambda x . x x \)? What is the semantic of \( (\lambda x . x x) (\lambda x . x x) \)?

For every set \(A\):

where \(I_A = \{ (x,x) ~|~ x \in A \}\).

Let \(F = (A,B,f)\) be a function.

Let \(G = (F \times A, B, g)\) be a function where \( g(f,x) = f(x) \).

23.34How do we know that our language is perfect?

"How to determine your new language is perfect?" http://lambda-the-ultimate.org/node/4395

24What

24.1Prolog implementation?

Predicate type(Name,TypeExp) defines types

24.2System state

The system state is essentially a big record/dictionary/tuple/product

24.3Model-theoretic principles: implementation, model, specification

An implementation is a finite model of a specification, where "model" means what it means in model theory. A specification is a big logical sentence in conjunctive normal form, in which each conjunct is a requirement (a property) that the system has to satisfy.

The computer, with some hints, should be able to derive a finite model from a specification.

The primary tools for formalizing an ontology are logic and set theory.

24.4Universal meta model? Example upper ontology?

In other words, we are looking for an upper ontology¹⁶ of program translation.

"X is a Y" means X is an element of the set Y.

"Every X has a Y" means there is a projection from the set X to the set Y.

Everything has a type.

Every finite thing can be represented by finitely many bits.

Every finite thing can be stored in a finite amount of space.

24.5Surrogate keys, equality, equivalence, identity

A surrogate key reduces identity check to equivalence check. A surrogate key enables us to concisely answer "which" questions. A surrogate key is a unique name. We consider two things different iff their identifiers differ.

The only thing we can do to distinguish the identity of abstract objects is to give them different names.

A surrogate key conflates equivalence and identity.

Without surrogate keys, there is no way for us to know whether duplicate records represent the same physical object. For example, suppose that there happens to be five (john, 30 years old) rows in the database. How do we know that all those five rows truly refer to the same person or are merely due to a programming error?

My conclusion is that every relation that represents concrete objects should have a surrogate key. A concrete object is an object that has material existence. Examples are people, cars, houses. Do bank accounts have material existence? No, a bank account is not a concrete object, but we care about the identity of a bank account: we care about distinguishing a bank account from another. I can open two bank accounts, and we care about that they have different identity. Two bank accounts differ merely by having different names (identifiers). Even if I equalize their account holders and their balances, they will still have different identifiers.

Every relation whose identity matters should have a surrogate key. When does identity matter?

If we may need to refer to a particular element of a relation, then the relation should have a surrogate key. If we need to ask "Delete which element?" or "Update which element?", then the relation should have a surrogate key.

There are two cases: where equality determines identity, and where equality is insufficient to determine identity. The first case usually happens when representing concrete objects. The second case usually happens when representing of abstract objects.

But are surrogate keys accidental complexity? Without surrogate keys, how is an information system going to answer "which customer", "which employee", "which book", etc? It is possible that two people have the same name. In a developing nation, it is normal for people to have several national IDs.

Two tuples \((a_1,b_1)\) and \((a_2,b_2)\) are equal iff \(a_1=a_2\) and \(b_1=b_2\). If the first component is a surrogate key, then we compare only the first component to determine equivalence, and we conflate this equivalence with equality.

In programming, we usually assume a closed world, that is, the program is all that exists.

X is a Y.

X has a Y that is a Z.

X is a relation.

All data is relational?

The system state may be distributed. For example, the system state may be a combination of the Java application state and the PostgreSQL database state. But this distribution of state is accidental, not essential. The specification language must have the same syntax for both updating a local in-memory relation and updating a relation in a remote database.

24.6Caching expensive intermediate result?

How do we do that?

24.7Easy things: generating Java data-transfer-object classes from specification

24.8Hard things: generating Java programs from specification

25A business-oriented variant

Prior arts: Ur/Web, Opa language.

Important features:

• website or web application user interface
• SQL join across several PostgreSQL instances
• check that SQL table exists
• check that page URL exists

HTTP, HTML, JavaScript, AJAX, client-server, and network connections are accidental complexity. What is essential is that the user wants to do something quickly. The programmer should care about what the user cares about.

URLs are accidental complexity. The user does not care about URLs.

The language user should only care about what the end user cares about.

The main task of the language user is to formalize the ontology implied by the mental model of the end user.

strcpy does what we want: it copies strings, but that is not all: it may overwrite a memory region it should not touch.

translate.rkt: Translator state opaque struct. Exports:

• (var-set! state name value) -> void
• (var-get state name) -> value

An interaction is either a command or a query.

(query q1
  (SELECT [d.a d.b d.c e.y e.z] FROM [JOIN d e] WHERE [= d.a e.x])
)
(page
  (url "/foo")
  (title "FOO")
  (body
    q1
  ))

TODO: Queries are shown with automatic AJAX pagination and editing (update, delete, insert)?

Requirement: accounting/tracing/logging of database modifications.

Thus, a query has to be mapped to a URL.

If ID is not given, then the ID is the URL.