1Story?

I have been writing Java code for a few years now. I always wonder whether there is a more concise way to write programs.

I have years of unfaithful on-and-off relationships with various languages, such as Haskell, Prolog, and Racket.

Prolog and Racket sparks joy in me when I write programs in them.

I think everyone has grievances with all languages.

How is the magical ellipsis in syntax-case implemented?

How is Typed Racket implemented?

In English, we often invent new vocabularies, but we rarely invent new syntax. English is a domain specific language whose domain is everyday human communication. English can act as its own meta-language. English contains a fragment of logic.

In a language, are we more concerned about expressing the problem or expressing the solution?

Racket struct has prop:procedure property that can be used to make a struct act like a procedure in an application expression.

Scribble is better than Pandoc? Alien technology, productivity multiplier? But I feel that Racket is a bit slow?

Demonstration of Racket as programming-language programming language:

  • Robby Findler impressively demonstrated1 Racket as a programming-language programming language.
  • Leif Andersen's video language2
  • William G. Hatch's "Rash": Reckless Shell Programming in Racket3

Is Scribble or Pollen45 the authoring system I have been looking for? Does my journey end where Matthew Butterick's journey ends? Patoline?6

It is regrettable that we have XML while S-expressions suffice, if not better.

I love Erik Meijer's crazy talk7:

  • 24:31 tenth man, Israeli intelligence, devil's advocate
  • 26:54 you should never stick around in a company for more than three years (unless you own it, perhaps)
  • 43:50 we pay more for plumbers than we pay more for software; it's crazy

I have become pragmatic. I see a class as a way to avoid repeating the first parameter of a collection of related functions. That a class corresponds to an entity in the real world is accidental. The essence of a class is to factor out a group of method parameters that often occur together.

Many programming language features are for grouping.

The purpose of a struct is to group parameters that always occur together.

The purpose of a class is to group the functions that use a common struct. A class is not about message passing or domain modeling. It is about grouping.

The purpose of a namespace or package is to group classes that are often used together.

The purpose of a module is to group definitions that are often used together.

The purpose of a library is to group namespaces that are often used together.

The purpose of an operating system is to group programs that are often used together.

This is a way of thinking: We can think of something as what it gathers.

I think Python's class is futile, self-defeating, and counterproductive: What is the point of having classes and instance methods if you have to type "self" as the first argument of the parameter list? The point of languages is to express ideas concisely. Class-based programming only works if the first "self" argument is implicit.

One annoying surprise in bash is that the following program doesn't work, perhaps because pipe starts new child processes?

echo foo | read

<2019-07-06> I think the most important thing in a programming language is to separate names and referents, that is, to be able to express things without naming them: anonymous classes, anonymous functions, anonymous modules, anonymous objects, anonymous everything. But it's cumbersome to do recursion without names.

All programming is ultimately imperative, because computers ultimately only understand machine instructions. All declarative programs must be translated into imperative programs before they can be executed. The translation can be done by compilation or interpretation.

"How" is the most important question after "why".

You can design programming languages, but at the end of the day, you have to implement an interpreter or translator.

2<2019-07-06> Racket macros

A syntax pair is not a pair of syntax objects, but is a syntax object whose datum is a pair. A syntax list is not a list of syntax objects, but is a syntax object whose datum is a list.

3<2019-07-06> Do not fix what is not broken, lest you break what is not broken

When I was young, I liked to tidy up source code.

I refactor something needlessly. The "problem" is that the code is "ugly", and my "fix" broke production. Looking back, I now think that was totally unnecessary.

4StackOverflow is harmful?

StackOverflow is full of bad advices and bad codes.

StackOverflow is great for expert developers who are trying to remember the details of a piece of code, but bad for novices who don't know of the consequences of what they are pasting into their terminal.

Ubuntu StackExchange answer writers are too eager to recommend sudo, and readers seem to be too eager to copy without understanding. The result: Broken Ubuntu installation. It did happen to a coworker of mine. I think we all had a coworker who mindlessly copied stuff from StackExchange only to break their operating system installation while not solving the original problem they set out to solve. It goes like this:

  • You have a problem.
  • You copy a snippet from Stack Exchange.
  • Now you have two problems.

5To write an IDE, we need a module system, not a type system

Module system is a prerequisite for writing an IDE and program analysis tool.

The setting/fixing of bindings/references/sites statically.

"Go to definition" and "find usages" is more important than type system.

Correct rename refactoring is more important than type system.

It is important to always be able to determine whether two names refer to the same thing. "This name is declared/defined in <somewhere>" "This name and that name refer to the same thing"

6Lisp and Scheme: converging?

Lisp now has static binding (lexical binding).

Scheme now has dynamic binding with "parameterize".

Some Lisp implementations have proper tail calls?

Lisp has multi-methods / generic functions for overloading (using the same name to work with several types). Scheme standard does not specify overloading? Guile has GOOPS. https://www.gnu.org/software/guile/manual/html_node/Methods-and-Generic-Functions.html Chicken Scheme.

I want to write "map"; I don't want to write "vector-map" or "<container>-map" for every container type. Can Alexis King's Hackett save me? She tantalizingly hinted8 at how Racket macros can benefit from Haskell and how Haskell can benefit from Racket macros.

7Expression-problem, OOP vs FP, subclass vs operation

OOP vs FP: OOP makes adding subclasses easy but makes adding operations hard. FP makes adding operations easy but makes adding subclasses hard. Which one is more likely in our case, adding subclass or adding operation?

// In FP, it is easy to add functions working with Shape, but hard to add a new type of Shape. data Shape = Circle | Rectangle

// In OOP, it is easy to add new subclasses of Shape, but hard to add methods to Shape. class Shape class Circle extends Shape class Rectangle extends Shape

What if we need to both add subclasses and add operations?

Sometimes it is possible to add an overridable method with default implementation.

Can we combine OOP and FP to get the best of both worlds, so that it is easy to add subclasses and it is easy to add operations? Or are we going to get the worst of both worlds? If Scala aims to combine OOP and FP, what is Scala's solution to the expression problem? How do we solve the expression problem in TypeScript? http://fileadmin.cs.lth.se/sde/people/gorel/misc/ExpProblemTalkPart1.pdf

8Names and referents should be separated

8.1Executive summary

The target audience is programming language designers and implementors.

I suggest that programming language implementors follow these principles:

  • Maximum composability and name-clash-freedom
    • The language must clearly separate names and referents. Name must not be a property of anything. Every language element must be able to exist anonymously. Every language element must be able to be referred to by a name. Example: JavaScript function vs C function.
    • The module systems must be a combination of JavaScript module system and Ocaml module system. Module must be first-class and anonymous.
  • Metaprogrammability
    • The language must be homoiconic. The language must comfortably model its own syntax.
    • The language must use Curry-style type system (extrinsic typing), not Church-style type system (intrinsic typing).
  • Usability
    • Overloading (giving same name several different meanings at the same time)?
    • The language must be lexically scoped.

We have two choices: Fix existing languages, or create a new language.

8.2Total separation between names and referents

8.2.1Example with functions

Consider this example:

// C
double add1 (double x) { return x + 1; }

// JavaScript
var add1 = function (x) { return x + 1; };

In C, the name "add1" is a property of the function. In JavaScript, "add1" is not a property of the function, but "add1" is a name that we use to refer to the function.

An analogous example: "Erik" is not a property of me. "Erik" is the name that people use to refer to me in a local scope (inside a room where I am the only person with that name). My existence does not depend on the name people use to refer to me. This is contrary to C that requires every function to decide its own name.

This separation between names and referents enhances composability. In programming parlance, when we say "everything should be first-class", we mean this total separation between names and referents.

A function must not decide its own name. The caller of that function picks a name that it uses to refer to that function. The same goes for modules and every other language element that can be named.

8.2.2Example with modules

The key message:

  • A thing (function, module, etc.) should not decide its own name.
  • The implementation must be able to load a file into an anonymous module.
  • The implementation must load the same file at most once.

If you satisfy those constraints, it will be simple to resolve name clashes in your language.

To avoid name clash, your module system must satisfy these:

  • The user of a module, not the module itself, decides what to call that module. A module must not name itself. A module does not have a name. A name is not a property of a module. A name is something that the user of that module uses to refer to that module.
  • A module can contain other modules.

As far as I know, the only languages with satisfactory module systems are JavaScript and TypeScript. Ocaml's anonymous modules and local imports are more satisfactory than JavaScript modules, but Ocaml as a whole is unsatisfactory because Ocaml infers module names from file names.

Most programming languages are unsatisfactory. A thing should not decide its own name.

// Java
package foo;      // Unsatisfactory: package foo decides its own name
class Cls {
}

-- Haskell
module Foo where  -- Unsatisfactory: module Foo decides its own name
data Bar = Baz

## Ruby
module Foo        ## Unsatisfactory: module Foo decides its own name
  class Bar
  end
end

// C++
namespace foo {   // Unsatisfactory: namespace foo decides its own name
}

The implementation must be able to load a file into an anonymous module:

The implementation must load the same file at most once. (Two files are the same iff their paths resolve to the same canonical path.) In this example, the contents of "foo.js" should be parsed exactly once.

A language used by millions of programmers must separate names and referents to avoid naming conflicts.

8.2.3Philosophical investigation

Designing anything good: Name is not a property of anything. Name is a linguistic artifact that we use to refer to something. A function does not have a name. A predicate does not have a name.

A language must clearly separate names and referents (the things that the names refer to).

If Prolog is to have anonymous predicates, then it works with second-order logic, no longer with first-order logic.

The job of a module is to disambiguate names. Example: which "member/2" do we mean?

8.2.4Does it make sense in a language with nominal typing?

Such as Haskell, Java, Ur/Web?

9Basic questions

9.1How is a programming language a language?

A language is a convention for representing thoughts.

Important concepts have shorter encodings. Who judges what is important? The speakers.

9.2Why is it easy to mix natural languages but not programming languages?

The reason it is easy to mix natural languages is that their syntaxes are the same. Their differences are superficial: the vocabulary. They all serve to talk about the common things in human experience: eating, trees, lions, dogs, foods. They share semantics.

Programming languages have wildly varying semantics. Some doesn't even have clear semantics.

9.3When are programmers happy?

Happiness happens when what the programmer thinks is important coincides with what the language designer thinks is important. For example, when I'm writing an accounting software, I don't care about the registers, pointers, memory addresses, and so on. In this case, I care more about ontology than about pointers.

10Pre-design

10.1How should we design a programming language?

Language design should start from semantics.

Names and referents should be separated (orthogonal).

A language is only as good as how it promotes communication.

What is communicated through a programming language? Two things: what things exist, and how those things should be manipulated.

Design is about trade-offs? Type inference requires limiting language expressivity?

10.2What are the design constraints of a programming language?

A programming language must be ultimately translatable to the machine's primitives.

Wirth's "Algorithms + Data Structures = Programs"?9

Barbara Liskov: "Our compilers today are not powerful enough to support or enforce semantic constraints.", answering question "Do you think that in those examples it’s worth having a refined subtype to explicitly encode the difference between the LIFO and FIFO semantics as part of a typing system or that would be something that would be annotated externally to the type system, like semantic constraints?"10

A programming language should not preclude efficient implementations.

10.3Literature research

What literature exists for programming language design?

What can programming language researchers learn from the philosophy of language?

Things to summarize:

Unanswered questions:

  • Is there a homoiconic statically-typed language? Does type system hamper homoiconicity?
  • Can we make high-level declarative language without garbage collection?

Making a programming language https://www.reddit.com/r/ProgrammingLanguages/comments/9ky7o6/writing_my_own_programming_language/e72qjll/ banzr: 'Racket is taught in universities to be used to write languages. Use "match" and "cases" to build the parser and interpreter. Good luck!'

2017 "Language Oriented Modularity: From Theory to Practice" http://programming-journal.org/2017/1/10/

2017 "Classless Object Semantics" http://researcharchive.vuw.ac.nz/handle/10063/6681

http://www.pl-enthusiast.net/2015/05/27/what-is-pl-research-and-how-is-it-useful/

11Program correctness

11.1What is correct?

11.2How do we know that our program is correct?

If we know that program \(x\) is correct, and we know that program transformation \(f\) preserves correctness, then we can infer that \(f(x)\) is correct.

Otherwise, our software may be correct but we don't know, or worse, incorrect and we don't know.

11.3Type systems, lightweight program reasoning systems

A type system is a sublanguage for reasoning about programs, for expressing some properties of programs.

11.3.1Is a type a set?

<2019-02-04> Phil Freeman asked "Can someone explain why people object to thinking of types as sets? I mean, I normally don’t, but it doesn’t seem incorrect necessarily." https://twitter.com/paf31/status/1092111216950992897

11.3.2When should we introduce a type system?

  • 2005 article "Introduction to Type Theory" pdf

11.3.3Is inheritance subtyping?

The short article [2] basically tells the user to read AbdelGawad's other works.

  • 1 [1] 1989, "Inheritance is not subtyping", pdf
  • 2 [2] 2013, "Inheritance is subtyping", pdf
  • Subtyping vs inheritance
    • Subtyping and inheritance are orthogonal concepts.

A language should provide both nominal and structural subtyping.

  • 2008, "Integrating Nominal and Structural Subtyping", pdf

We can define structural subtyping for C structs.

We can define layout types (almost like ASN.1):

layout {
    at byte 0;
    def var0 : little_endian int32;
    at byte 4;
    def var1 : big_endian int32;
    reserve 8 byte;
    skip 4 byte; -- synonym for reserve
    def var2 : int8;
    def var3 : array of 4 int8;
    align 16;
    def var4 : layout {
        reserve 16 byte;
        def var1 : int8;
        align 32;
    };
}

We can define intersection, union, concatenation, and composition/nesting of two layout types.

Why don't we just build ASN.1 into the language?

11.3.4Maximum polymorphism?

11.3.5Typing records

A record type can be thought of as a product type whose components are named.

If each value valN has type typN, then the record {key1=val1; key2=val2; ...;} has type {key1:typ1; key2:typ2; ...;}. For example, the record {name"John"; age=20}= has type {name:String; age:Int;}.

11.3.6Polymorphism is code generation

  • Consider translating id : a -> a to assembly.

    • If types define memory layout (bit representation), then the compiler must generate an id function for every a.
    • If the language uses runtime type tagging, then there doesn't have to be more than one=id= functions.

11.3.7Fixed points and recursive types

A thing \( x \) is a fixed point of function \( f \) iff \( f(x) = x \).

A function may have zero, one, or many fixed points.

A thing \( x : A \) is a least fixed point of function \( f : A \to A \) iff \( x \) is a minimum of the set of the fixed points of \( f \). The words "least" and "minimum" assume an ordering \( \le \). This ordering should be clear from context.

If \( f \) has exactly one least fixed point \( x \) with respect to ordering \( \le \), then we write \( \mu_\le(f) = x \).

The syntax \( \mu a. b \) means \( \mu_\le(\lambda a. b) \). The syntax \( \mu a. b \) is analogous to lambda expression syntax \( \lambda a. b \).

What is the ordering used in formulating the least fixed point of a recursive algebraic data type?

todo: equirecursive types and isorecursive types

11.3.8Benefits and drawbacks of static type checking

The benefits of types:

  • Types prevent stupid mistakes.
  • Types can be used to improve program efficiency.
  • Types are documentation for both human and machine. Types communicate intention to both human and machine.

The drawbacks of types:

  • Some safe programs don't typecheck.
  • Some programs become longer.
    • Haskell's type system complicates the AST decoration problem. In TypeScript, the AST decoration problem is trivial; you just add a field at runtime.

  1. Arguments for static type checking?

    1. What?

      • There are two camps:
        • DTL (dynamically typed language)
        • STL (statically typed language)
      • Every programmer is lazy, but differently.
        • People who use DTLs are too lazy to write the types.
        • People who use STLs are too lazy to do what machines can do, such as
          • detecting typos,
          • avoiding unintentional conversions,
          • tracing the code, 2 weeks later, to find out the type of a variable.
      • People who use DTLs are too diligent.

      They love to do what machines can do: type checking.

      • Static typing enables you to be lazier. Help the machine help you avoid work. By investing in a few keystrokes, you will get these in return:
      • The machine will catch more mistakes for you.
      • You can have an IDE that finds references correctly. This enables features such as "Jump to definition", "Rename", and even more fancy refactorings.
      • Moral of the story:
        • Let the machines do all the boring stuffs.
        • Be future-lazy, not present-lazy. Do things now so that you can be lazy later. Don't be lazy now only to regret it later.
          • People who organize their things are too lazy to spend mental effort later in a scramble to find things.
          • People who don't organize their things are just too lazy to do it, and would rather just experience regret in the future than experience some hardship now for a better future.
          • The sane solution to "too lazy to write types" is to pick a language with type inference, not to ditch types altogether.
          Don't throw the baby out with the bathwater.
      • This argument also applies to functional programming vs procedural programming. Indeed this argument applies to every technology. Adopting technology enables us to be lazier.
      • People buy tractors because they are too lazy to till their fields with hoes.
      • People use frameworks because they are too lazy to do the same plumbing again and again.
      • People strive to avoid side-effects in functional programming because they are too lazy to debug synchronization errors.
      • The only thing the human race isn't too lazy to do is to think about lazier ways of doing things.

    2. What?

11.3.9Prolog is ideal for writing a typechecker, and TypeScript is ideal for typechecking AST decorations, so we should fuse Prolog and TypeScript.

Abdullah pointed out to me that TypeScript interface is similar to Ocaml polymorphic variant?

  1. But there is Racket and its languages such as ProfessorJ, Datalog.

12Declarative

12.1Combining lambda-calculus and first-order logic: combining beta-reduction, unification, and backtracking

Anonymous function: \ x -> x + 1 Anonymous predicate: \ a b c -> f a, g b, h c fix f = f (fix f)

father_child(dad, kid). father_child(daddy, kiddo).

:- operator – father(daddy) – child(kiddo).

father_child dad kid father_child daddy kiddo father dad – child kid

father_child = \ dad kid father_child = \ Dad Kid -> Dad = dad, Kid = kid

"First-order logic without equality" https://math.stackexchange.com/questions/363168/first-order-logic-without-equality

"Differences between logic with and without equality" https://mathoverflow.net/questions/316648/differences-between-logic-with-and-without-equality

Isn't this Curry language? Curry's slogan is "A Truly Integrated Functional Logic Language"

Lambda-Prolog, Harrop formula Why was Harrop formula defined? What's so special about it? https://en.wikipedia.org/wiki/Harrop_formula

Lambda-Prolog

https://math.stackexchange.com/questions/2494645/lambda-calculus-combined-with-first-order-logic-notation-quantifiers-propositi

"But languages aren't tools! IDEs are tools. Languages are material. See FallacyOfTheRightTool." http://wiki.c2.com/?QuestForThePerfectLanguage

12.2Prolog predicate naming

blue(X) has(A,B) can_sing(A) version(A,B,C) person_name(P,N) index_fibonacci index_list_element

class_field table_column column_type

class(Atom) is true iff Atom is a referent.

table(Atom) has different namespace

class_field(Cls, F) :- table_column(T, Col), field_name(F, N), column_name(Col, N).

Metamodel A thing is modeled as an association list such as [a=b,c=d,e=f] alist_key_value([K=V|_],K,V). alist_key_value([_|R],K,V) :- alist_key_value(R,K,V).

alist_empty alist_tail alist_head alist_without_keys alist_size alist_merge

thing_prop(T,P) thing_prop_replaced(T0,P,T1) Use thing_prop_replaced(T,P,T) to get the property P of T

url_page

There is a difference between dif and \=: dif is coroutining. https://stackoverflow.com/questions/16560058/difference-between-x-y-and-difx-y But "coroutine" is an overloaded term. http://www.swi-prolog.org/pldoc/man?section=delcont

Prolog predicate naming problem when there is a compound word integer_integer_sum(A, B, C) basic_block__ssa_block()

12.3Prolog

How does Mercury do without assert/retract?11

1988, Towards functional programming in Prolog12. It defines several infix operators. "[…] The problem of evaluating expressions combining functions and predicates is investigated. Examples are provided to illustrate the discussion. The paper includes a prototype implementation."

2.7.1 "Axiomatizing Context-Free Grammars"13. See third paragraph: "the general statement made by the context-free rule […] can be summarized using relations on positions with the following logical statement […]"

12.4Reconciling functional and logic programming into declarative programming?

1996 publication "A Note on Declarative Programming Paradigms and the Future of Definitional Programming" html

12.4.1Example: Representing a predicate in lambda calculus

Lambda calculus with boolean logic extensions:

p = \ x -> x = "a" OR x = "b"

Prolog:

p(a).
p(b).

12.4.2Example: Representing a function in logic programming

inc(X, Y) :- X = Y + 1.

12.4.3The "satisfy" function

The expression "satisfy f" finds all x : a that satisfies f : a -> bool. Thus the type of "satisfy" is "(a -> bool) -> list a".

It is in principle possible to write such "satisfy" builtin for some lambda expressions.

satisfy (\ x -> x = "a" OR x = "b")
=> ["a","b"]

satisfy (\ (x : int) -> x >= 10)
=> [10,11,12,...] -- an infinite list

satisfy (\ (x : bool) -> true)
=> [false,true]

12.4.4A function is a relation, a relation is a function, so what?

A function \( (A,B,F) \) is trivially a relation.

A relation \( (A,B,R) \) is a function \( (A,2^B,F) \) where \( F(x) = \{ y ~|~ (x,y) \in R \} \).

13Interoperation

13.1Foreign function interface: working with C

13.2Working with existing systems

13.2.1Working with Java

13.3Interoperability between programming languages

14Functional programming language design

14.1"Let" introduces sharing?

"Let" determines how the AST (abstract syntax tree) turns into ASG (abstract semantic graph).

14.2Lambda calculus algebra what?

The algebraicity of the lambda-calculus14

an untyped lambda-calculus is a functor LC from sets to sets: to a set V (of free ”variables”) it assigns a set LC(V) of lambda-terms built out from V; this functor enjoys substitution, which turns it into a monad;

The idea that the notion of monad is suited for modelling substitution concerning syntax (and semantics) has been retained by many recent contributions concerned with syntax (see e.g. [BP99] [GU03] [MU04]) although some other settings have been considered.

14.3Algebra of ADT

Somewhat interesting https://stackoverflow.com/questions/9190352/abusing-the-algebra-of-algebraic-data-types-why-does-this-work

14.4Lambda calculus

Lambda calculus formalizes binding and substitution.

Follow Ben Lynn's lambda-calculus tutorial:

  • why use lambda calculus as theoretical basis (cool reasons!)

14.4.1Beta-reduction

  • reduce : E -> E
  • reduce ((\ x -> y) p) = reduce (y[x:=p])
    • y[x:=p] means y but with every bound occurence of x replaced with p)
  • reduce x = x otherwise

14.5Let-expressions

The let-expression let x1 = y1; ...; xn = yn; in z; desugars to (\ x1 ... xn -> z) y1 ... yn.

Let-expressions is for readability by humans.

Do we still need let-expressions if our program is well-factored?

14.5.1let-expressions may recur

I think letrec is ugly. All let-expression should allow recursion, like Haskell's.

https://stackoverflow.com/questions/28796904/whats-the-reason-of-let-rec-for-impure-functional-language-ocaml/28798040

14.6Sharing, laziness, full laziness, complete laziness, and optimal reduction

14.6.1Sharing

  • Should the programmer care about sharing?
  • sigma-calculus?
  • Should the programmer decide whether to share or not?
  • Is there a best sharing strategy?
  • Should the machine guess by heuristics?

Sharing affects performance, but does not change the result. Should we care?

14.6.2Example of sharing

Consider the expression letexp defined as let x = y in z;.

We want x to be shared iff doing so speeds up the reduction of letexp.

This is always the case:

  • If x occurs at most once in z, we always want x not shared.

These depend on circumstances:

  • If y is expensive, we want x shared.
  • If y is cheap, we want x not shared.

How do we define "expensive"?

14.6.3Lazy accumulation problem

sum a 0 = a
sum a

sum 0 = 0
sum n = n + sum (n - 1)

14.7Currying is not compatible with vararg and named parameters?

Vararg stands for "variable-length arguments".

Do we want currying?

Currying simplifies language user but complicates compiler writer.

The problems:

14.8System F, System F with subtyping, System F-omega

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

"System F is rich enough that the self-application \x.x x is typable." https://crypto.stanford.edu/~blynn/lambda/systemf.html

Brown and Palsberg, "Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega"

14.9Introduction to lambda-calculus?

  • unknown-year lecture notes "Lambda Calculus as a Programming Language" pdf

I thought lambda calculus could be summarized in one page, but Henk Barendregt wrote hundreds of pages about it. Is there more to lambda calculus than it seems?

  • 1994, 50 pages, pdf
  • 1991, 190 pages, pdf

14.10Extending lambda-calculus with various bells and whistles

  • Vectorial lambda-calculus

    • The 2013 article "The Vectorial Lambda-Calculus" pdf adds vectors and matrices and their types to lambda calculus.
    • The 2010 article "Semantics of a Typed Algebraic Lambda-Calculus" pdf available also mentions "vectorial".

  • 2016 article "System F-omega with Equirecursive Types for Datatype-Generic Programming" pdf

14.11Lambda calculus semantics?

14.12Optimizing lambda calculus?

14.13Ocaml

14.14Imperative subset

Haskell's ST monad enables us to embed a local imperative program in a functional program.

14.15Overloadable function application?

14.16Haskell woes

14.16.1Can't import type class instances explicitly

There is a reason.

14.17Monads, and Haskell type system limitations

14.17.1Should Nat (the natural numbers) be a subtype of Int (the integers)?

Intuitively, yes.

14.17.2<2018-10-01> ??? Signedness is a monad: conservatively extending naturals to integers

I think this is what we mean when we say "integer is a monad". I think what we are really trying to say is "signedness is a monad", that is, "we can conservatively extend the naturals to the integers by using the Signed monad".

We can write that in Haskell as follows (with some problems described later).

data Nat = Zero | Succ Nat
type Int = Signed Nat
data Signed a = Positive a | Negative a

instance Functor Signed ...
instance Applicative Signed ...

instance Monad Signed where
    return = Positive
    m >>= k = join_signed (fmap k m)

join_signed :: Signed (Signed a) -> Signed a
join_signed mm = case mm of
    Positive x -> x
    Negative x -> negate_signed x

negate_signed :: Signed a -> Signed a
negate_signed (Positive x) = Negative x
negate_signed (Negative x) = Positive x

f :: Nat -> Nat
f = ...

f_int :: Int -> Int
f_int = fmap f

We can have Signed Char, Signed String, etc., but those may not make sense.

The problem: Nat should be a subtype of Int, because everyone who knows arithmetics seems to think that way. We want f and f_int to be the same function. We don't want to type fmap, liftM2, and their ilk.

14.18Abdullah's dream language: Extending System F application beta-reduction rules to automate fmap and extend?

Add these inference rules?

  • If f : a -> b, and x : m a, and m is an instance of Functor, then f x beta-reduces to fmap f x.
  • If k : a -> m b, and x : m a, and m is an instance of Monad, then k x beta-reduces to k =<< x.

\[ f : a \to b , ~ x : m~a , ~ Functor~m \vdash (f~x \to_\beta fmap~f~x) \]

Suppose f : a -> b, and x : m (p a), and m is an instance of Functor, and p is an instance of Functor.

  • The rule beta-reduces f x to fmap f x.
  • Problem: The rule interferes with the Functor instance of (->).

14.19Some tentative plans: Create a language that compiles to Haskell?

15Functional programming research?

Problem: This chapter lacks a narrative.

Abbreviations:

  • CPS: continuation-passing style
  • FP: functional programming
  • OS: operating system
  • PFP: partial functional programming
  • TFP: total functional programming
  • TFPL: total functional programming language
  • TM: Turing machine

15.1Why total functional programming?

  • Can you sell me some TFP?
    • What is TFP?
      • TFP is functional programming with only total functions.
        • A function is total iff it is defined for every element of its domain.
      • TFP ensures that every function is total by constraining every recursion to be structural recursion.
        • Structural recursion is recursion with the constraint that every recursive call is syntactically smaller.
    • Why TFP?
      • The practical advantage of TFP is that it is easier (and therefore faster and less costly) to write provably correct programs in TFP compared to PFP or imperative programming.
        • This ultimately translates to faster time-to-market, lower development cost, fewer errors, fewer customer complaints, and higher customer satisfaction. (I know this sounds like bullshit. We should not underestimate the ways that humans can screw up.)
      • The theoretical advantage of TFP is that TFP has simpler denotational semantics compared to PFP because TFP has less bottoms to consider. [Turner2004]
    • Why not TFP?
      • A disadvantage of TFP is that it is not Turing-complete because all programs must terminate, but OSes don't terminate, but we can still write an OS in a TFPL using codata and corecursion [Turner2004] which are discussed in another section in this document.

[Turner2004] calls TFP "strong functional programming".

15.2Ramble

You should not read anything below this point. These are the drafts of my drafts. I think they should be included in this page, but I haven't worked them enough.

This is a questionnaire, not survey article: A preliminary survey of functional programming Caitlin Sadowski Daan Leijen https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-67.pdf

15.2.1History of lambda calculus?

Alonzo Church introduced lambda calculus in 1932 in [Church1932].

Why did Church invent lambda calculus? What was Church trying to do?

Notations have changed. Church wrote \(S_y^x U\) but we write \(U[x := y]\) for the same thing: the expression \(U\) but with every occurrence of free variable \(x\) replaced by expression \(y\).

[Church1932] credits a 1924 publication of Moses Schönfinkel for what we call currying: changing a multi-parameter function to a one-parameter function returning another one-parameter function returning yet another one-parameter function, and so on. Currying is changing \(f : (a,b) \to c\) to \(f' : a \to (b \to c)\) such that \(f(x,y) = (f'(x))(y)\).

See: Dana Scott's lambda-calculus timeline15.

See also: Wikipedia: Lambda calculus.

15.2.2might be too old

15.2.3Codata, corecursion, and coinduction

For more about codata, corecursion, and coinduction, see:

15.2.4Lazy, strict

  • The Church-Rosser property (Wikipedia, Mathworld), eliminates the difference between strict and lazy in a TFPL [Turner2004].

15.2.5A type theory is a formal system, not a branch of mathematics

There are at least two type theories: the Martin-Löf type theory, and the calculus of constructions [Bove2001]. I thought "type theory" was a branch of mathematics, like "category theory", "graph theory", and "number theory".

"Martin-Löf's type theory is basically a theory about sets in which it is possible to interpret a logic." [Nordstrom1988]

15.2.6Recursion and fixpoint

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

A text lecture describes how to obtain the factorial function as a fixed point of successive approximations.

Wikipedia: Fixed-point combinator. A fixed-point combinator enables anonymous recursive functions.

TFP rejects the definition fix f = f (fix f) because this is not a structural recursion.

Recursion is about fixpoint.

15.2.7The Eff language and monad-aware languages

Consider this passage from [McBride2015]:

[The Eff language lets] us write in direct style for whatever effectful interface is locally available, then obtain the computation delivered by the appropriate Moggi-style translation into an explicitly monadic kernel.

I think "in direct style" means that in Eff we can write f x to mean what we would write as x >> f= in Haskell, but with the Monad instance automatically inferred based on the locally available effects.

I think that passage suggests that the Eff language [Bauer2012] is related to the "monad-aware language" that Abdullah is trying to accomplish. The relation is that Eff infers the monad from the locally available effects. However, Eff's type system ignores the effects (like ML's type system) so this is probably not what Abdullah wants.

15.2.8Reading triage

http://semantic-domain.blogspot.co.id/2016/03/agda-is-not-purely-functional-language.html

https://en.wikipedia.org/wiki/Category:Term-rewriting_programming_languages

In a term-rewriting language such as Pure, we can write program transformation as part of the program. https://stackoverflow.com/questions/24330902/how-does-term-rewriting-based-evaluation-work

https://www.quora.com/What-are-examples-of-statically-typed-logic-programming-languages-ex-similar-to-Prolog

https://mathoverflow.net/questions/3920/what-does-it-mean-to-discharge-assumptions-or-premises

http://www.cs.nott.ac.uk/~pszvc/g54dtp/inductive_domain.v

https://stackoverflow.com/questions/145263/what-is-total-functional-programming

What is a computational effect?

Does totality really have anything to do with termination?

15.2.9TFP and Turing-completeness

We must distinguish between a Turing machine and its execution.

A TM needs a tape to run, but does not come with it. To run a TM, you have to supply a tape.

A tape is a finite sequence of tape symbols.

A step is a pair of configuration and tape.

A run is a sequence of steps. This sequence may be infinite.

A run of a Turing machine \(m\) with initial tape \(t\) is …

Instead of thinking about infinitely long tape with infinitely many blank symbols, we think that the tape is finite but the TM may at every step insert, update, or delete a cell.

A TM is finite by definition: a TM is a tuple whose each component is taken from a finite set. The description of a TM does not include the tape. The execution trace of a TM may be infinite. A TFPL can describe every TM just fine.

We can describe a Turing machine in a TFPL?

https://www.reddit.com/r/programming/comments/jvu2w/total_functional_programming_and_the_unimportance/

LTU: Total functional programming

https://news.ycombinator.com/item?id=12646390

https://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-still-theorems/

https://math.stackexchange.com/questions/111773/are-total-recursive-functions-recursively-enumerable

How do we write this "echo" program in TFP? Is it even total?

We can describe the infinite list of natural numbers [0,1,2,3,...] in a TFP.

f : Nat -> Nat
f n = n + 1

f : Nat -> Nat
f n = n

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type

http://www.cl.cam.ac.uk/archive/mjcg/plans/Coinduction.html

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

https://en.wikipedia.org/wiki/Initial_algebra endofunctor, F-algebra, initial object

probabilistic logic programming

15.2.10Metaprogramming

Spoofax vs Xtext vs MPS? http://www.metaborg.org/en/latest/ http://www.metaborg.org/en/latest/source/overview/examples.html

PEG (parsing expression grammar)

http://ttic.uchicago.edu/~dmcallester/foundations.pdf https://en.wikipedia.org/wiki/Foundations_of_mathematics https://web.stanford.edu/class/cs103/notes/Mathematical%20Foundations%20of%20Computing.pdf https://github.com/hoplon/javelin https://codon.com/consider-static-typing

15.2.11Structured editor

https://news.ycombinator.com/item?id=13773813

https://www.reddit.com/r/programming/comments/1tp83j/lamdu_structuralast_editor/

15.2.12Others

Compile and run Agda programs online.

15.2.13Positive and negative positions, strict positivity

In the function type \(A \to B\), we say that \(A\) occurs in a negative position and \(B\) occurs in a positive position. See CS StackExchange 42150.

For the strict positivity constraint of a data type definition, see these: CS StackExchange 55646, Agda Wiki: Strict positivity.

In a TFPL, there is no expression whose type is forall a. a.

exit : IO a

15.2.14Rewriting systems

A TFPL program is a terminating ARS. https://en.m.wikipedia.org/wiki/Termination_(term_rewriting)

SoftOption: normal forms and termination

SoftOption: lambda calculus and combinatory logic

There are at least two widely used confluent term-rewriting systems:

  • applicative, lambda calculus, beta-reduction
  • concatenative, postfix notation, PostScript, Forth

An expression is in normal form iff there is no applicable rewrite rule. See Wikipedia: Normal form (abstract rewriting).

The following hang function is not total. Why?

The expression hang x can be rewritten to hang x, so hang x is not a normal form, but this goes on forever, so hang x does not have a normal form, and thus hang x is not total.

This loop thing is not a function in the mathematical sense. Why is that?

loop : a
loop => loop

Consider this, where exit terminates the program.

The function crash also does not produce a Nat.

  • What is Scott continuity?

    • Why is it named "continuity"?

https://cs.stackexchange.com/questions/1371/scott-continuous-functions-an-alternative-definition

Girard's System F https://people.mpi-sws.org/~skilpat/plerg/papers/harper-system-f-2up.pdf https://www.reddit.com/r/haskell/comments/2zqtfk/why_isnt_anyone_talking_about_optimal_lambda/

Venanzio Capretta's partiality monad General recursion via coinductive types Venanzio Capretta 2005 "see the work by Barendregt and Geuvers [5] for a good exposition of technical issues of type-theoretic proof assistants" Coinductive types were first introduced in type theory by Hagino [34]

StackOverflow: What can Idris not do by giving up Turing-completeness?: "Dual to termination: while an inductive definition must terminate (by consuming all of its data) a coinductive definition must be productive - in practice this means, brieflt, that any recursive call must be guarded by a constructor. I've found this explanation to be the clearest (ymmv): adam.chlipala.net/cpdt/html/Coinductive.html" – Edwin Brady Apr 22 '14 at 17:58

Dependent Types and Multi-monadic Effects in F⋆ https://www.fstar-lang.org/papers/mumon/paper.pdf

Type Systems, Luca Cardelli http://lucacardelli.name/Papers/TypeSystems.pdf

Karl Voelker master thesis: practical programming with total functions

York CS wiki: FP researches

15.3Category theory and programming languages?

The section title needs a verb.

15.4Foundation of mathematics especially for programming?

Can we formalize "a program is an executable formal system" using Grue's map theory?

  • How is "false" represented?
  • How is "true" represented?
  • How is "conjunction" represented?

15.5Haskell strictness checker

15.6<2018-09-12> question for Abdullah

Do you know of anything that computes (generates code for) the products/sums of data-types? Do you know of any libraries that enable us to describe how to transform a data type to a related data type? Do you know of anything resembling template metaprogramming for Haskell that is not Template Haskell? For example:

data A = A1 | A2
data B = B1 | B2

-- <input>
generate data P = A * B
generate data S = A + B
-- </input>

-- <output>
data P  = P_A1_B1
        | P_A1_B2
        | P_A2_B1
        | P_A2_B2

data S  = S_A1 | S_A2
        | S_B1 | S_B2
-- </output>

15.7<2017-09-04> Scheme currying

15.7.1Abstract

We define the macros lambda/c, apply/c, and define/c, which are curried analogs of lambda, apply, and define, respectively. This way is simple, but it uses macros and it is limited to fixed-arity lambda expressions.

15.7.2The idea

The idea of lambda/c is this pattern:

(lambda/c (a) z) => (lambda (a) z)
(lambda/c (a b) z) => (lambda (a) (lambda (b) z))
(lambda/c (a b c) z) => (lambda (a) (lambda (b) (lambda (c) z)))
...

The idea of apply/c is this pattern:

(apply/c a b) => (a b)
(apply/c a b c) => ((a b) c)
(apply/c a b c d) => (((a b) c) d)
...

However, there is a difference: apply is an arity-2 procedure taking a procedure and a list, whereas apply/c is a macro that takes one or more arguments.

The idea of define/c is this parallel:

(define (a b ... y) z) = (define a (lambda (b ... y) z))
(define/c (a b ... y) z) = (define a (lambda/c (b ... y) z))

15.7.3The code

I tried this code on Guile 2.0.9 on Ubuntu 14.04.

(define-syntax lambda/c
    (syntax-rules ()
        (
            (_ (x) body ...)
            (lambda (x) body ...)
        )
        (
            (_ (x y ...) body ...)
            (lambda (x) (lambda/c (y ...) body ...))
        )
    )
)

(define-syntax apply/c
    (syntax-rules ()
        (
            (_ f)
            (f)
        )
        (
            (_ f x)
            (f x)
        )
        (
            (_ f x y ...)
            (apply/c (f x) y ...)
        )
    )
)

(define-syntax define/c
    (syntax-rules ()
        (
            (_ (f) body ...)
            (define f (lambda () body ...))
        )
        (
            (_ (f x ...) body ...)
            (define f (lambda/c (x ...) body ...))
        )
    )
)

15.7.4Example

After the above macros have been defined (by copying them to your REPL, for example), the following fragment should print three threes.

(define f (lambda/c (x y) (+ x y)))
(define g (lambda (x) (lambda (y) (+ x y))))
(define/c (h x y) (+ x y))
(apply/c f 1 2)
(apply/c g 1 2)
(apply/c h 1 2)

15.8<2018-04-07> Approximating general recursion in TFP

Here we are going to show how to approximate general recursive functions in TFP with the help of the following repeat and approx:

To approximate a general recursive function f : a -> b, we write a data type S_f and these three non-recursive total functions:

Then, we can approximate f as f_approx:

The count parameter can be thought of as a time limit or time-out, the number of iterations, the number of steps.

Here is an example approximation of the factorial function.

Here is an example approximation of bottom.

I conjecture that there is an algorithm that can transform every general recursive function into its begin-step-end form.

15.9what

15.10Programming language theory

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

16TODO Fix this incoherent Java ramble; don't read

16.1What

  • Make it work
  • Make it maintainable
  • Make it efficient (only if needed)
  • Make it reusable (only if there is demand)
  • You Are Not Gonna Need It until proven otherwise, but this does not mean you do not need to anticipate.
  • There are many ways to write code that do the same thing. Prefer the way that is the easiest to read and change and needs the least maintenance.
  • Don't write getters and setters. Move the computation into the class, or use public fields.
  • Corollary: Use public fields for your DTOs (or move the computation there). http://stackoverflow.com/questions/10240372/jackson-field-based-serialization
  • Make value classes have final fields and a constructor.
  • Use Java wisely ("Object-assisted procedural programming"). https://www.quora.com/In-Object-Oriented-design-are-void-methods-bad
  • OBPP ("Object-based procedural programming"), term coined by Peter DiSalvo.
  • Java is not OOP; Java is OBPP.

The Java language is the C language with automatic memory management and without preprocessor.

C:

Java:

The essence is the same, but Java reduces the accidental complexity.

Method chaining vs fluent Method chaining transforms the dot (method invocation) into semicolon (sequence point).

Fluent is embedded DSL.

16.2Candidate solution: source-to-source translation

16.3Candidate solution: binary interoperability

Translate Java class to LLVM IR.

Translate Haskell to LLVM IR.

Translate C to LLVM IR.

Java has JNI.

Constraints:

  • ABI-compatible with JNI: JNI C libraries works without recompilation.

Foreign.

What's wrong: I want to edit the syntax tree. I don't care about spacing.

The name is structural editor. projectional editor.

https://www.facebook.com/notes/kent-beck/prune-a-code-editor-that-is-not-a-text-editor/1012061842160013/

http://www.lamdu.org/

http://projectured.org/

16.4Improving the Java language

Too much software is written in Java.

Xtend

Kotlin

IDE support

Top-level methods.

16.5Metaprogramming

{% raw %}
    msg = "Hello";
    c = Class.new;
    c += {{ int foo; }};
    c += {{
        void sayHello ()
        {
            System.out.println($msg);
        }
    }};
{% endraw %}

16.6Old

This is my opinion on how to best use Java.

Java, when used properly, should not be more verbose than C. Java should be thought of as enhanced C. It adds these features:

  • namespacing
  • garbage collection
  • exception
  • limited functional programming
  • reflection (should be documented thoroughly when used)

and it removes these features:

  • preprocessor
  • separate header files

Java sucks least when used as a mainly procedural programming language.

Subclassing, public fields, getters, setters, statics, mutability, and big classes are not evil in and of themselves. What is evil is writing code without understanding why you write it that way. The key to good programming is understanding why the code is the way it is.

With documentation, understanding data is easier than understanding control flow.

A maintenance engineer translates requirement changes to software changes. Software consists of program code, database schema, documentation, and so on. A software is maintainable iff a reasonable requirement change translates to a reasonable software change.

For example, an application may now have to handle ten times the traffic it was designed for.

If, in 10 years, your application will never handle more than 10 requests per second, but you split your application into 10 JVMs communicating with JSON-RPC, you're wasting too many resources.

16.7Example of namespacing

This is a module in C. Note that each procedure name is prefixed with point_.

This is the module in Java. Note that now you don't have to prefix your method names with point_ because it already lives in the class Point.

16.8Another example

16.9Mixin

Use extend or mixin if and only if you want all subclasses to benefit from enhancements of the base class.

A tradeoff is that unsafeSetHp is public.

16.10Unrelated

Field stores data. Method does work. Classes groups fields and methods.

A class groups methods that share parameters. The fields are those shared parameters.

A Java class is equivalent to a C struct and the functions whose first parameter is that struct. In C, those things are usually grouped into one C file, so a Java class is practically equivalent to a C file. Static field in Java is global variable in C, but without the name conflict.

C #include translates to Java import, extends, and implements. implements X imports X's default methods into this module. extends X imports X's fields and methods into this module. import static imports X's static methods into this module.

Java 8 interfaces can be used as mixins. Use default methods.

A mixin is a contract "if you give me X, I'll give you Y."

Every method is a contract: If you give me X, I'll give you Y.

Getters and setters provide "lazy fields" and "computed fields".

Java can be used with edit-compile-reload-refresh. Java can hotswap.

IDE makes navigation easy.

A class is an instantiable module.

The aim is to maximize understandability and minimize duplication. Sometimes, reducing duplication makes the code incomprehensible.

a.b(c) is a syntactic sugar for b(a,c). Implicit first argument.

Exception is structured goto.

https://www.reddit.com/r/learnprogramming/comments/1f0g2b/eli5_the_main_differences_between_oop_and/

https://www.reddit.com/r/learnprogramming/comments/tocjf/procedural_programmer_me_needs_help_making_the_oo/

16.11Can process fix incompetent people?

16.12Java-Haskell interoperation

https://wiki.haskell.org/GHC/FAQ

https://wiki.haskell.org/HaskellImplementorsWorkshop/2016

16.12.1State of the art

LLJVM?

https://github.com/Frege/frege Haskell-like language

http://eta-lang.org/ port GHC primitives to Java?

Sorted from the most desirable (highest level):

  • Source-to-source translation.

    • Write a Java source interpreter in Haskell.
    • Map Haskell code to Java.

Write a JVM in Haskell.

Translate both Java and Haskell to a common lower-level language such as LLVM.

Core-to-bytecode.

JNI-to-FFI.

16.13Haskell-to-Java

http://mmhelloworld.github.io/blog/2013/07/10/frege-hello-java/

The Frege language. The Eta language.

Haskell => Java?

Core => Java?

Module => Class

Data type => Static inner class

Value > instance of =Thunk

Data constructor => Class extending the class corresponding to the data type

A value definition in a module => a static final Thunk field in the class

A class => A class

A member of a class > An instance field of the Class; the type of the field is =Thunk

A class constraint => A dictionary argument whose type is the class

Case match => if instanceof

Map Int and Int32 to a Thunk producing a java.lang.Integer. A Haskell program assumes that Int is a two's complement signed integer at least 30 bits wide.

16.13.1Java-to-Haskell

https://github.com/Frege/frege/wiki/Calling-Frege-Code-from-Java

Java method -> foreign import

Message-passing view of Java objects

16.14Architecture

Every Java program is a sequence of statements.

Every Java program is equivalent to one long main class?

A block is a sequence of statements.

class Name
    int prop
    // Generates:
    // int prop
    // int getProp ()
    // void setProp (int)
end

16.15Understanding factoring

Imagine writing your program as one long main method. It is almost certain that you will find duplicate blocks.

Two duplicate blocks can be factored into a method. Two methods with the same parameters can be factored into a class.

What is an optimal factoring of that program? The factoring is wrong iff the same change needs to be performed more than once. A program can also suffer from modification anomaly.

There are prime fragments: fragments that cannot be factored into smaller parts.

16.16OOP as a special case of FP

Object and closure are equivalent.

o.m(a0,a1,...) -> m o a0 a1 ...

16.17Functional multimethod

Statically checked.

collide (a : Asteroid) (b : Asteroid) = ...
collide (a : Asteroid) (s : Spaceship) = ...
collide (s : Spaceship) (a : Asteroid) = collide a s
collide (s : Spaceship) (t : Spaceship) = ...

True : Bool.

False : Bool.

Ord Bool.

Bool x, Bool y |-
    Equal x y =
        match x y in
            False False -> True;;
            True True -> True;;
            _ _ -> False.

LessThan False False = False.
LessThan False True = True.
LessThan True False = False.
LessThan True True = False.

IfElse False t f = f.
IfElse True t f = t.

And False x = False.
And True x = x.

Or False x = x.
Or True x = True.

Not False = True.
Not True = False.

Min x y = IfElse (LessThan x y) x y.
Max x y = IfElse (LessThan x y) y x.

Table Employee.

Column Id Employee |- Bigint Id.
Column Name Employee |- String Name.

Column name Employee, type name |- Read name From resultSet = Get type name From resultSet.

Column name Employee |-
    Member
        (Tuple name (Read name From resultSet))
        (Read Employee From resultSet).

Main |-
    source = Connect "jdbc:postgresql://127.0.0.1/test",
    resultSet = ExecuteQuery source "SELECT * FROM employee",
    Member tuple (Read Employee From resultSet),
    Print tuple.

?- Main.

Ord a, Ord b |- min a b = if lt a b then a else b

a : Asteroid, b : Asteroid |- collide a b = ...
IF
    a, b : Asteroid
    AND
    s, t : Spaceship
THEN
    collide a b = ...
    collide a s = ...
    collide s t = ...

define multimethod collide with parameters
    a, b : Asteroid
    s, t : Spaceship
where case parameters matching
    a b -> ...
    a s -> ...
    s a -> ...
    s t -> ...

16.18Java

a.m(b) and m(a,b) are equivalent. The dot is a syntactic sugar for implicit first argument, plus virtual dispatch.

The changes that must be made to implement a feature. The program is well-factored if no change is duplicated.

A maintainable software does not have to be object-oriented, but it has to be well-factored. A well-factored program prevents the same modification from being duplicated.

Factorization reduces information duplication.

Depending on dependable things simplify your program. I know someone who used a SQL database but didn't want to depend on it, so he wrote application-level joins everywhere.

A software is maintainable iff it is simple to change. Being able to start, stop, and restart quickly (in just a few seconds) also helps.

16.18.1SQL

Mutable fields.

Column a
    name : String
    read : a -> ResultSet -> ()
    write : ResultSet -> a -> ()

Table a = [Column a]

read : Table a -> a -> ResultSet -> ()
write : Table a -> ResultSet -> a -> ()

interface SqlCallable2<A, B>
{
    void call (A a, B b) throws SQLException;
}

class Column<E>
{
    String name;
    SqlCallable2<E, ResultSet> read;
    SqlCallable2<ResultSet, E> write;
}

16.18.2Annoyances of local variables

  • Java can't infer the type of local variables
  • Local variables aren't final by default

16.18.3Example of under-factored program

What if my_schema or employee change?

What if SQL syntax changes; for example, what if a committee decides to change SQL SELECT to CHOOSE? We assume it's unlikely, so we don't design our program to anticipate that.

16.19Extract covariant expressions into variables

What if employee.computeSalary changes?

What if we want to print to aPrintStream instead of System.out?

What if salary type changes from long to BigInteger? We assume it's unlikely.

16.20Extract covariant blocks into method

Two blocks that must change together.

becomes

Things that change together should be grouped together.

Constructors are methods too.

If two methods share a common parameter, the parameter can be extracted into a field.

If two classes share a common field, a class can be extracted.

Static methods are reusable.

Instance methods force you to instantiate the class.

16.21Implications of architecture on security

A popular trend: split front-end and back-end. Write front-end in NodeJS, write back-end in Java, front-end calls back-end via JSON HTTP API. Front-end runs on visitors' browsers. Back-end is open to public.

You cannot secure the application. If you cannot secure the hardware running the software, all bets are off.

  • 16.21.1Foo(143w~1m)

16.21.1Foo

Java is a procedural programming language.

The only reason we don't write everything in one big method is maintainability.

A code is easier to understand if it doesn't mix abstraction levels.

Names relate to things the reader already knows.

Java does not have C#'s extension methods.

Java as procedural programming with implicit first argument.

object.method(arg1, ...) = method(object, arg1, ...)

Principles make decision-making easy (not necessarily correct). Principles are heuristics.

Cohesion is the most important characteristic of a class. The purpose of a class is to group a working set (variables that often change together), and the methods that use those variables.

The risk of modifying code?

The larger the change, the bigger the risk.

If you are using object mapper like Jackson, changing a field to final can break your code. (You must annotate.) That's why I avoid reflection.

Microrefactoring. Small steps.

Abstraction is not a mere indirection. yegor256??? Abstraction allows you to say a lot with a little code.

16.22Mitigating the risk of changing code

Don't just change old code.

Write new code that works with the old code. Deprecate the old code. Delete the old code.

16.23Maintainable code

The problem is working with too many details at once.

Mixing HTTP-handling code (such as the Servlet API 3.0) with your business logic will cause readability problem. If a method contains getCookie and business logic, you're in for maintenance problems.

Java is more verbose than Haskell, but it doesn't mean that you can't create maintainable Java programs; it doesn't mean that your Haskell programs will automatically be more maintainable. If you suck, your code will be just as bad.

Java is a procedural language. Problems begin when people try to force object-oriented paradigm to Java.

16.24Writing program backwards

If you're a shop, you can try putting all your pricing logic into one class:

  • Every buyer whose age is 60 years or greater gets a 10% elder discount.
  • Every buyer (unique phone number) is a first-time buyer (who has not bought anything) gets 10% newcomer discount.
  • For simplicity, discount percentages are added before applied to the original price.

At this point you don't care about how to compute buyer_age and buyer_is_first_time. You simply want to express the pricing rules as a simple Java code that a programmer can easily understand.

To compute the buyer's age, we need his/her date of birth and today's date. Use JodaTime.

Then we need to figure out how to get today's date, and so on, and then you arrive at this method:

If you need something in a method, but it's not that method's responsibility to compute it, then it should be a parameter of that method.

There you have it: a straightforward, readable, maintainable, easily changeable pricing rule for your online business. A straightforward translation.

Filling the fields is someone else's problem.

Internationalization:

Do you need to be able to change the discounts without recompiling the program? You don't. Instead of making it configurable, make compilation and deployment fast, easy, and automatic, and just recompile. There is less room for mistakes if you keep it in one place that is easy to see: the source code. The compiler will also help catch mistakes.

Now you figure out how to compute buyer_age.

The name of a class doesn't have to be a noun.

A constructor parameter states that the class depends on a feature.

A class describes a feature.

A Java class corresponds to a C source file. This is as if you could put multiple C source files inside a Java class. And you can put many Java classes inside a Java class. Think of a class like a folder for C source files; it groups things to help programmers understand the code, not as something that corresponds to an object.

16.25Crucial question

If there are many ways of writing programs that do the same thing, why choose a particular way?

More maintainable.

16.26Use snake case

Class name: My_class_name

Field, method, and variable name: my_method_name

Maintainability is done by limiting ugliness inside a class.

It is possible to write maintainable Java code. It will only be a bit more verbose.

16.27Making a Java virtual machine

17Programming language design mistakes?

What is a design mistake? Does a design mistake exist? Or all that exists is trade-offs/compromises?

Assembly is not fun to use, but is it a design mistake? How else could it be done in the 20th century, other than wishfully thinking of telepathic machines?

17.1Justifying the creation of yet another programming language

A new programming language should fix unforeseen design mistakes in existing programming languages. It should not repeat their design mistakes. Therefore we should collect the design mistakes so that we can avoid repeating them.

What is a mistake? How do we know it's a mistake?

We realize something is a mistake when we find a better way.

Mistakes are always discovered by hindsight. We don't know it's a mistake until long after we have done it.

17.2Common design mistakes

17.2.1Ignoring programming language theory and research

Some mistakes are because the language designer is ignorant, lazy, or in a hurry.

17.2.2Dynamic typing

Dynamic typing speeds up prototyping but precludes translation to code that is as fast as statically-typed codes.

Static typing is about allowing the compiler to make simplifying assumptions to emit faster code. We can work faster with simplifying assumptions. For example, if we can assume that people don't mind being killed, we can kill all people, but that assumption is like the assumption that user input is always valid.

Dynamic typing is a design mistake? Type inference goes back to 1958. ML has type inference since 1973. It's 2018. There is no excuse for ignoring 60 years of research. See WP1, WP2.

17.2.3Lack of metaprogramming support?

17.2.4Lack of symbol overloading (ad-hoc polymorphism)

Scheme and Haskell lack convenient symbol overloading. Haskell requires you to make a type class for ad-hoc polymorphism.

Without overloading, clashing names need to be prefixed manually.

17.2.5Mutable by default?

17.2.6Non-first-class constructs

Object-oriented programming is a design mistake?

  • a.b() should not mean "call method b of object a"
  • a.b() should mean "get the function a.b, then call it".

  • a.b() should mean (a.b)().

    • m = a.b; m(); should mean the same as a.b().
    • Functions should be first-class. Methods should not exist. Fields are enough (with function types). It should be possible to assign to methods.

Statements are a design mistake. They should not exist. Only expressions should. Xtend and Haxe do this right. - Can we replace statements with expressions in existing imperative languages without breaking backward compatibility? - But C has WP:Comma operator? - We can use lambda calculus for imperative programming. - Treat the statement separator (here we use semicolon ;) as an operator (function with infix syntax) that sequences the effects of two expressions. - For example: - Let a be an expression. - Let b be an expression. - Thus a;b is an expression. - The value of a;b is the value of b. - The effect of a;b is the effect of a followed by the effect of b. - Semicolon is associative: (a;b);c = a;(b;c). This also holds for the effects.

17.2.7Virtual machines

Virtual machines are a design mistake. Instead, do semantic mapping: map a program in language A to an equivalent program in language B while preserving the meaning.

17.2.8More than one way to do something

"There is more than one way to do it" is a design mistake.

17.2.9Disallowing multi-line string literals

Languages should allow CR/LF in string literals.

17.2.10Not allowing extra leading or trailing commas

Allowing extra commas make Git diffs less noisy.

17.2.11Not separating names and referents

Example: C functions, Java classes, Haskell modules.

JavaScript does not make this mistake.

17.3Java

17.3.1Overcomplicated Java Virtual Machine

JVM does too much. JVM bytecode verification is the compiler's job, not the VM's. Does JVM bytecode verification even add any security? Isn't JNI a bigger security hole?

17.3.2Working against programmers

Java presumes that the programmer is not only untrustworthy but also an idiot.

Programmers make mistakes, but they aren't idiots.

17.3.3Throwing away the good parts of C++

17.3.4Weak functional programming (allowing partial functions)

Allowing partial functions is a design mistake.

17.4C and C++

In the 1970s these were tolerable: memory was limited, tools didn't exist. In 2018 these aren't tolerable.

  • Unattainable standard.
  • Pile of workarounds.
  • C++ compilation is abysmally slow. #include <iostream> expands to 10000 lines.
  • C pointer declaration syntax for pointers and arrays is a design mistake.
  • Conflating pointers and arrays.
  • Leaving a lot of things undefined.
  • Zero-terminated string is a design mistake.
  • Parsing requires symbol resolution and type checking.
  • Header files. They should be automatically generated from C files instead.
  • Preprocessor works on text, not on C/C++ AST.

17.5Haskell

  • Template Haskell is a mistake.
    • Instead, we should have a metaprogramming library, and generate hs files.
  • Haskell compilation is slow.
  • Haskell module system is a design mistake.
  • GHC: If A depends on B, and B changes without changing API, then A still requires recompilation.
  • Bottom inhabits every type including the supposedly empty type data Void.

17.5.1Not leveraging user-defined isomorphisms

I want this:

data A = A0 | A1
data B = B0 | B1

isomorphism "iso" between A and B is
    A0 ~ B0
    A1 ~ B1

instead of this:

Explicit isomorphism may help reduce newtype boilerplate.

17.6Prolog

Difference between rules and queries. Files contain rules. Interpreters accept queries. This is a mistake that prevents local contexts.

Instead of assert and retract, Prolog should have scopes: with(Rules,Query).

Instead of Prolog modules, Prolog should have dictionaries and JavaScript-like require(Path).

17.7what

A problem with current programming methodologies is that they don't capture the higher-level properties of software, such as the architecture. For example, how do we write, in a way that the computer can exploit, this statement: "The fields of class C correspond one-to-one with the columns of database table T."?

https://www.drmaciver.com/2009/01/criticizing-programming-languages/

Lua design mistakes

Picking different syntax for the sake of being different

for elem in table surprisingly doesn't work, but this is for greater cause; the for syntax is surprisingly consistent (iterators, which are coroutines)

Distinguishing statements and expressions

Why do new language designers still repeat design mistakes?

17.8Lisp design mistake: having separate data and function cell

18Total mess

18.1Catching mistakes; checking; proving; reasoning; type systems

18.1.1Curry-style extrinsic typing instead of Church-style intrinsic typing

Types help, but they are not the essence. Types are a means of writing better programs, not an end to be achieved for its own sake. Type should not be a property of an expression. Prefer Curry-style (domain-free) type system to Church-style (domainful) type system.

"Domain-Free Pure Type Systems" https://pdfs.semanticscholar.org/e638/74519839d4f2baf27f95078fc50ed0540fed.pdf

But, if we don't have types, how do we resolve overloading? We can't resolve overloading without context. The only context we have is what variable has what type.

For example, this is an example essence of a business logic:

discount_percent P = 0
  + (if old P then 10 else 0)
  + (if student P then 10 else 0)
  + (if pregnant P then 10 else 0)

The meaning is as in mathematics: all numbers are real numbers. Realization then produces a restricted subset of that description that works for all numbers whose magnitude is smaller than 2^63. A program is a restricted (realized, finitized) mathematical description. Example: The mathematical description f x = x + 1 works with all real numbers. The program works with all natural numbers from 0 to 2^64-1. The realization of a mathematical function (A,B,F) is simply a finite subset of it: (A',B',F'), where A', B', and F' are finite. Even if you use arbitrary-precision arithmetic, you are still limited to the memory of the machine. For example, if the machine only has 1000 bytes of memory, then it can only realize number smaller than 2(1000 * 8).

18.1.2What is a type? Understanding what a type is from how it is used

Mathematically, A type is a set whose membership is syntactically decidable.

Engineeringly, A type gives meaning to bit patterns.

A type encodes meaning into bit patterns.

  • For example, consider the bit pattern 11111111.
    • It means -1 as an int8.
    • It means 127 as an uint8.
  • Types help translate programs.

Type system helps machines help us. We shouldn't focus on type systems. We should focus on logic. We should focus on making machines help us. The question is not how to make a good type system. The question is how to offload the job as much as possible from humans to machines.

A programming language is a formal system. A type system is a formal system. Therefore a type system is a formal system embedded in a bigger formal system that is a programming language.

Programming languages have semantics, even if it is implicit.

A type defines the memory layout (bit pattern) of its values.

A type constrains values and expressions.

A type determines what values a function can take/give.

There are also other uses of types.

The question is: What is a type? What principles should we follow when we design a language?

18.1.3Church types and Curry types

Things to read:

18.1.4Row polymorphism

Why is it called row polymorphism? Where is the row? See "Objects and Aspects: Row Polymorphism", Neel Krishnaswami pdf

In the following, the function set_name_r is row-polymorphic. The function set_name_n is not row-polymorphic.

type Person = { name : String; age : Int; };
type Company = { name : String; location : String; };

set_name_r : String -> {name:String; r;} -> {name:String; r;};
set_name_r new_name {name=n; r;} = {name=new_name; r;};

set_name_n : String -> {name:String;} -> {name:String;};
set_name_n new_name {name=n;} = {name=new_name;};

john : Person;
john = { name="John"; age = 20; }

joe : Person;
joe = set_name_r "Joe" john;

not_person : {name:String};
not_person = set_name_n "What" john;

abc = { name="ABC"; location="1 ABC Way"; };
def = set_name_r "DEF" abc;

Without row polymorphism, we would have to write set_name twice: once for each type.

  1. Row polymorphism vs subtyping

    https://cs.stackexchange.com/questions/53998/what-are-the-major-differences-between-row-polymorphism-and-subtyping

  2. Row polymorphism vs structural subtyping

    https://news.ycombinator.com/item?id=13047934

18.1.5what

18.1.6Parametricity

18.1.7Subtyping

A subtyping relation is an ordering of types.

So what? That is technically correct but that doesn't give any insights.

A subtype is an ordering that follows the Liskov substitution principle?

18.1.8Type-checking

  • Every type checking algorithm is unification (logic programming).
    • If the programmer annotates a term, use that annotation.
    • If the a term is not annotated, annotate that term with a freshly generated variable.
    • Unify everything according to the typing rules.
    • See Algorithm W in WP:Hindley–Milner type system.

18.1.9Algebraic subtyping?

It means P(X) => P(Y) for every predicate P. Liskov substitution principle. Does it mean "X is a subclass of Y" or "X is an instance of Y"?

18.2What

18.2.1Introduction

  1. Goal

    The goal is to build a usable formal language up from lambda calculus.

    A formal human language is a formal language that humans use to precisely (unambiguously) communicate technicalities to other humans in a way that is also feasible to machine translation using classical compiler techniques.

  2. Examples of extending lambda calculus

    1. TODO Study OCaml

      Caml begets Caml Light begets OCaml.

  3. Principles

    1. Refer to mathematics, logic, and English.

    2. Solve the root cause; don't hack.

    3. Interoperate with existing systems. Improve existing systems. Enable replacement, but don't require it.

18.2.2Functional programming

Every functional programming language is lambda calculus plus plus.

Functional programming is lambda calculus plus plus.

18.2.3What we do when we understand programs

When we are trying to understand a program, what we actually do is we run an abstract interpretation of the program in our head. We model the program in our internal language of thought: logic, most likely first-order logic. "Abstract interpretation" has a specific meaning; see Wikipedia.

18.2.4Modeling

  1. Prolog meta-thinking: logic, language, query, and modeling: how many parameters should we use?

    Consider these models:

    0 john_loves_mary
1 john_loves(mary)
2 loves(john,mary)
3 subject_verb_object(john,love,mary)

    If we want to pattern match on it, or quantify it (existentially or universally), then it should be a parameter. Example:

    • "Who does John love" can not be answered by 0.
    • "Who loves who" can not be answered by 1.
    • "Who does what to whom" can not be answered by 2.
    • "Who does what to whom at what time" can not be answered by 3.

    Thus the number of parameters in our model depends on the complexity of the queries that we anticipate. Thus when designing a logic program, we should begin with the queries that we want to anticipate.

  2. Modeling everything = name-property-value + subject-verb-object + time

    Model of everything Entity-attribute-value I call it "name-property-value" to get in line with the terms used in philosophy https://en.wikipedia.org/wiki/Entity%E2%80%93attribute%E2%80%93value_model

    name-property-value

    "The color of mycar is black." :- multifile name_property_value/3. name_property_value(mycar, color, black). name_property_value(mydb, type, database). name_property_value(mydb, subtype, postgresql). name_property_value(mydb, is_a, database).

    I think, if the knowledge base is big, it will be very confusing to trace which rule causes which name to have which property.

    name_property_value(N, host, V) :- name_property_value(N, type, database), name_property_value(N, spec, Spec), member(host(V), Spec).

    "Show me all databases." ?- name_property_value(E, type, database). % press semicolon repeatedly

    "X is a database" vs "The type of X is database" (The attribute "type" of X has the value "database")

18.2.5Ramble: What is programming language expressivity?

What if we define language expressivity this way?

"J-expressive" means "expressive with respect to language J (judge)"

Language S (strong) is more J-expressive than language W (weak) iff the shortest interpreter for J in S is shorter than the shortest interpreter for J in W, without caring about speed.

Language A is more complex than language B iff A is more B-expressive than B is A-expressive.

Prolog is simple to reason but hard to implement? Java is hard to reason but simple to implement? It is easier to write Prolog interpreter in Java than to write Java interpreter in Prolog. But how does Prolog's simplicity enables us to write better programs? If a language is more complex, shouldn't it be more expressive/powerful? What is the relationship between complexity, expressivity, and power? What is expressivity?

I can make a language more complex without adding expressivity, by adding features that don't fit with the language?

18.2.6Present in ACM SIGPLAN conferences?

ACM SIGPLAN POPL/PLDI/SLE https://www.sigplan.org/Conferences/ seem to be the right conferences to disseminate this idea, but I should clean up this article first.

18.2.7SWI-Prolog stuff?

  1. What should SWI-Prolog modules be?

    We want these to separate names and referents:

    • anonymous modules
    • anonymous predicates
    • load file content into an anonymous module

    consult(++FilePath, –Module)

    SWI-Prolog module/1 option of load_files/2 enables the caller to separate a name and a module. A module still has to be named, but now the module user decides the name.

    A module is a dictionary.

    SWI-Prolog dynamic module may be saving grace.

    Prolog has dynamic scoping. Dynamic scoping is a mistake. Prolog should have lexical scoping.

    Explicit linking directive modulename_filepath(foo, library(mylib/foo))

  2. Prolog module clash = game over? Can logtalk save the day?

    https://logtalk.org/rationale.html

    • comparison of the module systems of various Prolog implementations

18.2.8Ideas?

The problem of C++ is that it tries to do too much.

18.2.9Proglang mess

A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification

https://pdfs.semanticscholar.org/8935/8a00317f9e380abe02b9f0d04536a6cd3121.pdf

https://www.google.co.id/amp/s/amp.reddit.com/r/ProgrammingLanguages/comments/6gsacs/any_info_on_compiling_lambda_calculus_to_other/ Compiling without continuations

Prolog dcg vs Haskell happy vs parsec https://www.quora.com/Is-Prolog-still-the-best-logic-programming-language-as-of-2016

https://www.mercurylang.org/documentation/papers.html http://www.cse.chalmers.se/~oloft/Papers/wm96/node2.html Google search pure log. pro.

Purifying prolog IO using state threading Sequential print(W0,M0,W1), print(W1,M1,W2) Parallel print(W0,M0,W1), print(W0,M1,W2), join(W1,W2,W3)

http://batsov.com/articles/2012/02/19/package-management-in-emacs-the-good-the-bad-and-the-ugly/ http://milkbox.net/

Transforming AST to ASG by hashing every syntax element.

The one devops tool to rule them all

DADL is what we want for devops?

Extracting Instruction Semantics via Symbolic Execution of Code https://github.com/trailofbits/codereason "CodeReason is a semantic binary code analysis framework and toolset."

Opalang's database support is interesting.

https://opensource.com/tools/supply-chain-management

2006 article "Poitín: Distilling Theorems From Conjectures" https://www.sciencedirect.com/science/article/pii/S1571066106001149

1984 publication "A Logic for the Russell Programming Language" https://ecommons.cornell.edu/handle/1813/6433

ICSE 1982 article "Capturing more world knowledge in the requirements specification" https://dl.acm.org/citation.cfm?id=800254.807765

ICSE 1987 article "Process models, process programs, programming support" https://dl.acm.org/citation.cfm?id=41765.41767

On the power-series expansion of a rational function http://matwbn.icm.edu.pl/ksiazki/aa/aa62/aa6233.pdf

  • Example of ontology for accomodation; related to data modeling:

http://ontologies.sti-innsbruck.at/acco/ns.html#overview

Should we just use Opa or Ur/Web? Which should we use, Opa or Ur/Web? https://en.wikipedia.org/wiki/Opa_(programming_language) "It can be used for both client-side and server-side scripting, where complete programs are written in Opa and subsequently compiled to Node.js on the server and JavaScript on the client, with the compiler automating all communication between the two." (emphasis mine) https://en.wikipedia.org/wiki/Ur_(programming_language) "[…] from a single program produces server code, browser client code and SQL code specific for the chosen database backend."

Inspired by English, XQuery, and ML.

Use Landin offside rule to infer closing tags:

let page title body =
  <html>
    <head>
      <title>{title}</title>
    </head>
    <body>{body}</body>
  </html>
in
if subpath begins with /url1/url2 {
  if subpath begins with /url3 {
    if request method is GET { (* This handles GET /url1/url2/url3 *)
      let strong text = <strong>{text}</strong> in
      page "Hello" <div>{strong "Hello"}</div>
      <html>
        <body>
          {strong Hello}
    }
  }
}

<html>
  <body>
    {strong Hello}

+ GET /url1/url2/url3 {page "title" <strong>hello</strong>}
+ GET /url1/url2/url4 {page "url4" <strong>what</strong>}

We don't need to create a new surface syntax. We can shallow-embed the DSL in Ocaml.

We need a new surface syntax if we want to generate routing data structure at compile time. The choice for the data structures are:

  • We can use a hash table.
  • We can use a prefix tree.
match-criteria { what-to-do-if-match }

expr returning node

Program ::= if Condition { Program } | serve PageExp
Condition ::= true | subpath begins with String | client accepts Accept | request method is String
String ::= <non-space>+ | Quote <non-quote>+ Quote
PageExp ::= Node | { MLNodeExp }
  • "Scala by example" online book

I think most people believe "I don't really understand what my coworkers do but I believe they're doing it well."

  • Stages of academic productivity:
    • You don't build on any past work. You start things and abandon them soon after. You redo your own work. You redo others' work without knowing it.
    • You know other people' work, but pride prevents you from even considering to study that work. You want to reinvent everything.
    • You learn to build on your past work.
    • You study other people's work, but you think you can do better.
    • You learn to build on other people's work.
    • You look for others who might share your interests.
    • You don't care whether it's you or someone else who solves the research problem. All you want is to see it solved.

You write a parser in C. You rewrite the parser in Scheme. You rewrite the parser again in Haskell. Then you search for the essence of programming. Then you stop writing parsers. Now you write the grammar instead, and find a way to generate the parser from the grammar. You also look for a way to generate the pretty printer from the grammar. You find Prolog.

  • citizen researcher, "academic spelunker"

https://lptk.github.io/programming/2018/10/04/comprehending-monoids-with-class.html

http://hazel.org/ "Hazel is a live functional programming environment featuring typed holes."

http://tomasp.net/blog/2018/programming-interaction/

1999 article "Essence—An LR Parser Generator for Scheme" http://s48.org/essence/doc/essence.pdf "The generated parsers result from the general parser by an automatic program transformation called partial evaluation." Holy shit.

https://mortoray.com/2012/07/20/why-i-dont-use-a-parser-generator/

  • "One key aspect that bothers me with many of the tools is the requirement to have a distinct first lexing phase." I agree. That requirement is an unnecessary restriction for 2018 computers.

2018 article "SweetPea: A Language for Designing Experiments"

polymorphism 2018 article "A Principled approach to Ornamentation in ML"

POPL 2018 talk "Formal Methods and the Law": formalizing code-based law "[…] computational analysis of these formalizations may discover previously overlooked tax avoidance techniques."

can ocaml polymorphic variants be used for row-polymorphic record types?

2015 article "A Crash Course on ML Modules" https://jozefg.bitbucket.io/posts/2015-01-08-modules.html

mapping between Haskell type classes and ML modules 2006 article "Modular Type Classes":

  • "We present a smooth integration of type classes and modules that provides a foundation for future work on incorporating type classes into ML and a proper module system into Haskell"

https://people.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf

"Code of ethics doesn't influence decisions of software developers" https://www.reddit.com/r/programming/comments/9myr6a/code_of_ethics_doesnt_influence_decisions_of/

miniKanren for compilers? Relational programming for compiler writing/

2013 article Spoofax vs Xtext http://msdl.cs.mcgill.ca/people/hv/teaching/MSBDesign/201314/projects/Leonard.Elezi/report/reading_report.pdf

http://flint.cs.yale.edu/cs421/case-for-ml.html http://troydm.github.io/blog/2014/03/29/writing-micro-compiler-in-ocaml/ https://stackoverflow.com/questions/14632870/creating-a-compiler-learn-ocaml-or-stick-with-java-c-c

https://people.mpi-sws.org/~rossberg/sml-vs-ocaml.html#exceptions

OCaml looks good ML language family: Why 'a tree instead of tree a?

Spoofax vs Xtext vs MPS?

https://www.metaborg.org/en/latest/

  • What you give Spoofax: language definitions.
  • What Spoofax gives you: the IDE for the languages.

!!! Write program transformation systems in Prolog or Mercury.

Clear https://www.metalevel.at/prolog/data

Logic programming is natural match for program checking.

Transform

entity(Name, Fields) entity(what,[ [id,int32,nullable], [name,varchar(byte(60))] ]). each(sql_java_type_eqv, [(int32,int), (int64,long)]). let(F = long_pred_name, F(int32,int)).

into

field(Entity_name, Field_name, Sql_type,

https://stackoverflow.com/questions/50512673/prolog-variable-as-functor

entity_field(Entity, [Name, Type | Opts]) one_to_many(A, B) relation_1_n_entity_entity(Rel, A, B)

We can change Prolog's search strategy by using metapredicates? Cite?

Prolog record type? Prolog beta reduction? SWI-Prolog has IDEs

"The power of Prolog" https://www.metalevel.at/prolog Timeline: Prolog, miniKanren, Godel, Mercury?

https://www.researchgate.net/publication/221266897_A_Compiler_Written_in_Prolog_The_Veda_Experience http://faculty.cooper.edu/smyth/cs225/ch7/prolog.htm https://dtai.cs.kuleuven.be/projects/ALP/newsletter/archive_93_96/net/grammars/compiler2.html https://docs.racket-lang.org/reference/match.html http://esumii.github.io/min-caml/index-e.html http://adam.chlipala.net/mlcomp/

External type checking in the style of Erlang Dialyzer.

A type checker is a function from AST to Extended AST.

Resource should be freed as soon as it is not used.

How should we think of compile-time checking?

  • Compile-time errors predicts runtime errors.
  • Compile-time errors preclude runtime errors.

Type checking is a special case of program checking.

https://medium.com/@daveford/what-i-want-in-a-type-system-1316a78365b

Compile-time is a model of runtime. We don't model hardware errors.

Using DCG to parse CST

The principle: the rules must incorporate the parsed input. Don't remove information.

I changed my mind. Write a DCG metainterpreter that adds location data to the token stream. Separate the concerns.

"Separating concerns with metainterpreters" may be a worthy talk.

"Separating cross-cutting concerns with Prolog metainterpreters"

A CST node is either F(Code) or F(Child1, …, ChildN) where F is a functor and each ChildK is a CST node and Code is a character code An error node is error(Message, A, B) It means that the parser encounters an error and resyncs to B A is the offending subinput

exp(plus(M, N)) :- … exp(number(F,R)) :- … exp(digit(D)) :- …

Use [plus,M,N] instead of plus(M,N) Comments

data CST = Space Char | Digit Char | Number CST CST | Plus CST CST | Error Msg CST CST

exp :: String -> CST

It is possible to reconstruct the input string from the CST.

What is the difference between Scheme match library and ML pattern matching?

Experiment

A=[1,2],append(A,B,C) infinite B=[1,2],append(A,B,C) infinite C=[1,2],append(A,B,C) infinite In order for C to be length-ground when append/3 exits:

  • A and B are length-ground, or
  • C is length-ground.

append(A,B,C)

S ::= <empty> | S a s(A) :- append([S0,[0'a],S1],A), s(S0), s(S1).

  • A terminal cannot be empty.
  • Each right-hand side must contain at least one terminal. We require that every rule consume at least one character. This is so that the recursion is always decreasing.
  • The generated parser requires that the input be length-ground. If the input is not length-ground, the parser may not terminate.

number ::= digit ; digit, number.

expression ::= number ; expression, "+", expression.

% Preprocessing.

% Terminal. translate(STRING, t(CODES)) :- string(STRING), string_codes(STRING, CODES).

% Sequence. translate((A, B), s(TA, TB)) :- translate(A, TA), translate(B, TB).

% Choice. translate((A; B), c(TA, TB)) :- translate(A, TA), translate(B, TB).

% Nonterminal. translate(CALL, n(CALL)) :- callable(CALL), functor(CALL, Name, _), \+ member(Name, [',', ';']).

% TODO

% Terminal.

translate(Input, Before, After, STRING, append([Before, CODES, After], Input)) :- string(STRING), string_codes(STRING, CODES).

translate(V_Input, V_Before, V_After, Call, Phrase) :- compound_name_arguments(Call, Functor, Args), compound_name_arguments(Phrase, Functor, Args_1),

rule_body__clause_body(Var_Input, Rule_body, Phrase) :- true , compound_name_arguments(Rule_body, Functor, Args) ,

TODO handle newline code_location_effect(Code, A, B) :- location_right(A, B).

node(Loc_before, Loc_after, Input, Remain)

The location can be inferred from the difference list.

node(Input, Remain) :- …, append(Parsed, Remain, Input). // codes_location(Parsed, Loc0, Loc1)

Embed P in H Embed H in P op let 1200 op val 1200

let x = 1. x(1). let f(X) = X + 1. f(X, X + 1).

Extend SWI Prolog checker library Erlang-Dialyzer-style checker for Prolog

Prolog for computing taxes.

http://www.swi-prolog.org/pack/list?p=func

https://github.com/SWI-Prolog/issues/issues/14

"Prolog's Control Constructs in a Functional Setting — Axioms and Implementation" https://www.cs.ox.ac.uk/publications/publication1149-abstract.html

Example of using Xtext, MPS, Spoofax http://voelter.de/dslbook/markusvoelter-dslengineering-1.0.pdf

Software requirement does not change? It is we who failed to discover the requirement? It is we who failed to discover the underlying reality? But how do we distinguish between design and overengineering?

Functional query expression language all_rows_of(Table) all(Table) from(Table) Table (just Table) project(Columns, InTable) = OutTable join(T1,T2)

Relational query formula language table_row(Table, R) table_columns_projected(T,C,R)

https://dtai.cs.kuleuven.be/projects/ALP/newsletter/archive_93_96/net/exts/monad.html

Prolog gui in logtalk?

https://stackoverflow.com/questions/19832464/what-are-the-minimum-maximum-integers-in-gprolog http://www.swi-prolog.org/pack/list?p=plgi http://lambda-the-ultimate.org/node/3813

Picat language?

Dbpure similar to plspec

"(Parnas, Shore & Weiss 1976) identified five definitions of a 'type'" https://en.wikipedia.org/wiki/Data_type

18.2.10How many arguments does id have?

Iceland_jack asked: https://twitter.com/ErikDominikus/status/1074009681553707008

0 in SKI combinator calculus

1 in Haskell / ML / Ocaml / F# / Scheme / JavaScript / untyped lambda-calculus

2 in Idris / Lean / GHC Core / System F / Coq

18.3Taxonomy of programming languages?

  • Dichotomies
  • Having denotational semantics vs not
  • With vs without runtime type information
  • Curry-style, implicit typing, optional typing, gradual typing
  • Church-style suggestive typing, meaningful typing
  • Statement vs expression
  • Imperative vs declarative
  • Value vs reference (referentially transparent vs not)
  • By value spaces?
  • Principled vs unprincipled
  • Designed by person vs by committee

18.4What should a programming language be?

How should Haskell be improved?

  • How do we use Haskell without fmap, ap, and other annoying syntactic baggages? How do we have Maybe(A) = A union {Nothing}? (The original question that started it all.)
  • What does a set-theoretic type system look like? (The consequence of wanting Maybe(A) = A union {Nothing}.)
  • What if the denotational semantics directly involve functors and monads?
  • Why should we use that language / write programs that way?
  • Is there an efficient implementation?

How should lambda calculus be implemented? What is an optimal implementation?

18.5What is the essence of programming language constructs?

18.5.1Records, dictionaries, ordering, function model

A record's components are ordered. A dictionary's entries are unordered. Both can be modeled by a function from the set of keys to the set of values.

A record {a:1, b:2} can be modeled by the function \((K,V,F)\) where \(K = \Set{a,b}\) and \(V = \Set{1,2}\) and \(F = \Set{(a,1), (b,2)}\).

18.5.2The essence of dictionary is finite function

Clojure gets this right?

Left-hand side of an application may be:

  • a dictionary,
  • a lambda, or
  • a finite left-biased union of arbitrarily many dictionaries and lambdas, or
  • a union like that but right-biased.

18.5.3Dictionary, map, associative array, record, finite function, hash table

  1. Clojure maps are applicable like functions.

    A very interesting fundamental idea.

    Clojure has nice map syntax: (m k) for accessing k.

    Maps are isomorphic to functions. We update a map. Updating a function is simple:

    A Prolog deterministic binary predicate is like a Clojure map.

18.5.4What is an array?

What is the difference between an array, a string (byte string vs character string), and a sequence?

C does not have built-in arrays; it has pointer arithmetics. An "array access" expression p[i] is a syntactic sugar for the pointer arithmetic dereference expression *(p+i).

Is a C++ vector an array?

18.5.5Comments

Humans and machines should understand the same thing. Comments should not be used very much. All explanations should be understood by both humans and machines. If a programmer has to resort to comments, then the language has failed to be expressive enough to express that comment.

We require less comments in languages with static type-checking.

A variable's type is a partial answer to "What does this variable mean", "What is this variable", and "What are the possible values of this variable". It formalizes the programmer's assumptions.

18.6Growing a programming language?

2006, "A growable language" "programming language designers should plan for such growth, along with the growth of a user community" https://dl.acm.org/citation.cfm?id=1176621

Racket manifesto? Racket language-oriented programming?

18.7What is a paradigm?

A mindset. A way of thinking. A way of looking at things. A lens through which we look at everything.

18.8Leverage existing infrastructures instead of creating from scratch

Instead of creating a programming language from scratch, we should leverage existing programming language infrastructures.

So far we think Prolog is the best for sketching languages with abstract syntax (that is, when we care about the semantics and do not care about the concrete syntax). The concrete syntax can always come later. Pretty concrete syntax will not console the programmers traumatized by ugly semantics. It would be like marrying a handsome but rotten man: the hype turns into regret after a few weeks.

18.9Logic programming

Prolog is at least second-order, as exemplified by its call/2.

We should program in logic because logic is the nternal language of thought?

18.10What is the best programming language?

This is what I think the best programming language would is like, as of <2018-12-30>.

general feel: Prolog + Haskell

Katahdin - runtime syntax manipulation

supercompilation + partial evaluation + compilation by abstract interpretation

user-extensible unification?

Type system: Curry-style, not Church-style. More like Erlang Dialyzer or TypeScript than Haskell. Users should be able to write their own program checkers and program transformations.

Module and import system: ld linker script, JavaScript, Nix import by lambda parameter name, Dhall, OCaml local import.

Syntax: Landin offside rule?

Pure + nondeterminism + JavaScript module system

18.11What are some interesting programming languages?

18.11.1Do we really have to read these fragmented sources?

19Bibliography

  1. Lambda Jam 2015 - Robby Findler - Racket: A Programming-Language Programming Language #YOWLambdaJam https://www.youtube.com/watch?v=hFlIl0Zo234↩

  2. https://www.youtube.com/watch?v=OZXslNVaCOQ↩

  3. https://www.youtube.com/watch?v=yXcwK3XNU3Y&t=448s↩

  4. https://docs.racket-lang.org/pollen/↩

  5. (fourth RacketCon): Matthew Butterick — Like a Blind Squirrel in a Ferrari https://www.youtube.com/watch?v=IMz09jYOgoc&feature=youtu.be↩

  6. http://patoline.org/↩

  7. One Hacker Way Rational alternative of Agile - Erik Meijer https://www.youtube.com/watch?v=2u0sNRO-QKQ↩

  8. "Hackett: a metaprogrammable Haskell" by Alexis King https://www.youtube.com/watch?v=5QQdI3P7MdY↩

  9. https://en.wikipedia.org/wiki/Algorithms_%2B_Data_Structures_%3D_Programs↩

  10. https://www.infoq.com/interviews/barbara-liskov↩

  11. https://www.mercurylang.org/information/doc-latest/mercury_trans_guide/AssertRetract.html↩

  12. ftp://obaluae.inf.puc-rio.br/pub/docs/Publications/88_AI_Furtado_SINPLAN.Not.pdf↩

  13. http://www.mtome.com/Publications/PNLA/prolog-digital.pdf↩

  14. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.311.3514&rep=rep1&type=pdf↩

  15. https://turing100.acm.org/lambda_calculus_timeline.pdf↩