Confluence (rewriting system)

Multiple paths between a source and target term via rewrite rules.

As in the Church-Rosser theorem (ie, ordering in which reduction rules are applied doesn't matter in lambda calculus).

Weak vs strong normalization (rewriting system)

Following is weak normalizing:

1) S -> S S
2) S -> A

because there exists at least one path by which normal form is reached:

S -> S S 
  -> A A         (by 2)

But this is not strong normalizing because, the rewriting can potentially go on infinitely. For example:

S -> S S 
  -> (S S) S     (by 1)
  -> ...

— Strong normalization => no matter what order of rewrite rules we use, it will eventually lead to a normal form within a finite number of rewrites.

Untyped lambda calculus is not normalizing. Due to the famous divergent terms. It is not even weakly normalizing since given (λx. x x) (λx. x x), the only applicable rewrite rule is that of application and it would simply diverge further.

On the other hand, simply typed lambda calculus is strongly normalizing.

—

• Strong normalization implies weak normalization, but not the other way.
• Normal form => no more applicable rewrite rules. Irreducible.

Ref:

• https://cs.stackexchange.com/questions/68080/what-is-the-difference-between-strong-normalization-and-weak-normalization-in-th
• https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting)
• https://www.cse.chalmers.se/~abela/talkMcGill2012Normalization.pdf

Point-free functions

• aka tacit programming
• A style of writing functions where the function arguments are never explicitly mentioned.
• The function is made as a combinator.
  • via function composition operations.

Eg: A function to find factorial of a number

A 'normal' style function:

-- Haskell
fact :: Int -> Int
fact 0 = 1
fact n = n * fact (n-1)

λ> fact 5
120

A point-free style function: ¹⁰

fact :: Int -> Int
fact = foldl (*) 1 . enumFromTo 1

λ> fact 5
120

Weak head normal form

From here:

Weak-head normal form means: evaluate it until you reach the outermost constructor.

Eg:

Also see this.

Bifunctor

• Short for 'binary functor'¹.
• Functors of two arguments.
• A functor whose domain is a product of two categories.

Haskell got it in Data.Bifunctor:

class BiFunctor f where
  bimap :: (a -> b) -> (c -> d) -> f a b -> f c d

Incompleteness of subtyping in Java

Array types should be invariant, but java compiler enforces only the covariant part during its type checking phase. Java has got

   S <: T 
------------
 [S] <: [T]

The contravariance check is done at run-time.

So programs like this:³:

public class Foo {
  public static void main(String[] args) {
    Object[] oarr = "hi,hello".split(",");
    oarr[0] = 42;
  }
}

will compile fine, but would result in runtime error:

Exception in thread "main" java.lang.ArrayStoreException: java.lang.Integer
        at Foo.main(Foo.java:5)

This is a design choice that some people consider to have been not so cool.

See this and this.

Type inference

• aka type reconstruction

Principal type

Most general instance of a type: 'makes the smallest commitment about the values of type variables tha yields a well-typed term' Eg:

a = λf:Y. λx.X. f x

a by itself is not well-typed.

But if we have a map like:
σ = {Y↦X→X, X↦X}

σ a = λf:X→X. λx.X. f x

which is well-typed.

This is the most general instance of a.

Notation:

• σ ⊑ β: unifier σ is less specific (ie, more general) than unifier β.

Principal unifier: Most general unifier

• σ such that ∀α, σ ⊑ α

First-class values

With first-class values in a programming language, both the following are possible:

• Can be passed as arguments to functions
• Can be stored in data structures

Logical relations

Refs: link link

Strong normalization (??) of STLC is not provable with induction (??) but is with logical relations.

W-types and M-types

• Looks like W-types are just inductive types as in Coq

• And M-types seem to be coinductive types

• 'M-types can be derived from W-types': https://en.wikipedia.org/wiki/Inductive_type

See:

• https://ncatlab.org/nlab/show/W-type#WTypesInTypeTheory
• https://ncatlab.org/nlab/show/well-founded+relation

More:

• https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed_official1.pdf
• https://www.cs.uoregon.edu/research/summerschool/summer16/notes/AhmedLR.pdf
• https://cs.brown.edu/people/bgreenma/resources/notes/logical-relations-greatest-hits.pdf

Kind

A kind is a type of types.

From https://serokell.io/blog/kinds-and-hkts-in-haskell

they show the arity of a type (if we think of that type as a function).

Concrete types are like values and polymorphic types are like functions.

Subtyping

• aka subtype polymorphism
• Principle of safe substitution
• 'subset semantics': a way of interpreting subtype relation

—

S <: T:

• S is a sub-type of T
• T is a super-type of S
• Set of S-values is a subset of set of T-values (aka subset-semantics)
• S is more informative than T
• Values described by S are also described by T
• Eg: S=squares, T=rectangles
  • All squares are also rectangles

—

Subsumption rule:

   s: S
 S <: T
---------  (T-SUB)
   s: T

—

Subtyping relation:

• Must be reflexive and transitive
• Record type: Can make S by adding more fields to T => S <: T
  • Smaller type (ie, type with lesser number of values) is the subtype
  • Subtyping => we are kind of further restricting set of possible values
  • Width subtyping
• Subtyping for functions => variance comes to play
  • Says under what circumstances can a function of one type can be used in place of another.

—

Sense of relation reversed for arg type (contravariant) but remained same for result type (covariant).

 T1 <: S1        S2 <: T2 
──────────────────────────
      S1→S2 <: T1→T2

(Go from conclusion then it's easier to remember this rule)

Intuition behind this rule:

f: S1→S2 means f is a function that accepts values of type S1.

This means f would accept values of a subtype of S1 as well. If T1 <: S1, we have:

S1→S2 <: T1→?

Now, considering the result value. f gives a value of type S2. Any value of type S2 is also a value of a supertype of S2.

If S2 <: T2, we have:

S1→S2 <: T1→T2

• No arg should 'surprise' the function.
• No result should surprise the context (to which the value from f would be given).

—

• Top: Maximum element of subtyping relation
  • Supertype of all types

Variance

• Covariant: 'Ordering of component types preserved'
• Contravariant: Ordering of component type reversed
• Bivariant: Both covariant and contravariant
• Invariant: Neither covariant and contravariant

Consider a type operator T and types A and B.

• T is convariant if A ≤ B means T(A) ≤ T(B)
• T is contravariant if A ≤ B means T(B) ≤ T(A)
• Invariant => mutable?? As in anything can happen??

https://old.reddit.com/r/programming/comments/lkmhy/understanding_covariance_and_contravariance_in/

• 'Java array subtyping problem – which is resolved in Java by doing a runtime check at each array mutation operation.'

Axiom K

There is only one proof equality.

• Not valid in homotopy type theory

https://www.pls-lab.org/en/Axiom_K_(type_theory)

Misc

• catamorphism: fold (banana)
• anamorphism: unfold
• hylomorphism: function made with both fold and unfold operations
• Endofunctor: A functor mapping a category to the self-same category.

Types, Categories, Topologies, Knots, etc

From an article.

Operational vs denotational semantics

• Synthetic guarded domain theory (SGDT)

Recursion vs corecursion

They are duals of each other.

Recursion:

• Kinda 'top-down': Go down till a base case and build up from there
• Folding

Co-recursion:

• Kinda 'bottom-up: Accumulator style. Start from a point and build from there
• Unfolding

—

More:

• Classical (co)recursion - Downen, Ariola @ JFP'2023
• https://blog.thomasheartman.com/posts/corecursion-and-anamorphisms
• https://softwareengineering.stackexchange.com/questions/144274/whats-the-difference-between-recursion-and-corecursion

ITP vs ATP

References

• https://www.pls-lab.org/