General Programming Questions

Glossary

Simply-Typed Lambda Calculus: Every term is explicitly typed. Types are base types and function types. Terms are lambda abstractions, applications, variables, and annotated terms. Values are variables applied to values and lambda abstractions with values. Functions cannot be polymorphic. It is strongly normalizing. (Contrast to dependent typing or languages with polymorphic types.)

Weak normalization property: “A rewrite system [has] the weak normalization property, meaning that for every term, there exists at least one particular sequence of rewrites that eventually yields a normal form, i.e., an irreducible term.” (Wikipedia)

For example, S -> (SS); S -> A has the weak normalization property because you can always reach A by never using the first rule. But it does not have the strong normalization property because the first rule will take you down a rabbit hole.

Strong normalization property: “A rewrite system has the (strong) normalization property or is terminating if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates with an irreducible term, also called a normal form.” (Wikipedia)

Neither the strong nor the weak normalization property: Look at the pure untyped lambda calculus - (\x.xx)t rewrites to tt. So, (\x.xx)(\x.xx) rewrites to (\x.xx)(\x.xx) and never terminates.

de Bruijn indices:

Variable occurrences are represented by numbers instead of strings or letters, the number indicating how many binders occur between its binder and the occurrence. For example, we can write id as -> 0, and const as -> -> 1 using de Bruijn indices. The advantage of this representation is that variables never have to be renamed, i.e., -equality of terms reduces to syntactic equality of terms. The disadvantage of using de Bruijn indices is it is rather cumbersome to manipulate terms with free variables. Although we can use indices unbound by a lambda to indicate that a variable is free, these indices are relative - whenever we traverse a term and go under a lambda, these references must be updated accordingly.

– LambdaPi

Dependent function space:

The ordinary function space (->) goes from an arbitrary domain to an arbitrary range. However, the range can’t depend on the domain. For example, you can express length :: String -> Int but not id :: a -> a.

The dependent function space (forall) allows the range to depend on the domain. For example, id would be forall a :: * . a -> a. Give me an a of base type * and a value of that type a and I will return a value of that type a. (h/t LambdaPi)

Similarly, we can represent the family of types Vec1 a, Vec2 a a, and so on using some function that takes an Int and returns the appropriate Vec. But we saw that ordinary functions don’t let the range depend on the domain. So, we need a dependent function. Specifically, forall a :: * . forall n :: Nat . Vec a n. So, the forall a . b is just a more permissive version of a -> b.

Finally, id for Vecs can be typed as id :: forall a :: * . forall n :: Nat . Vec a n -> Vec a n. The last part is just an ordinary function since the range does not depend on the domain. However, we can still write it as a dependent function: id :: forall a :: * . forall n :: Nat . forall v :: Vec a n . Vec a n. All of a sudden, what was a function is now a type.

Prolog

Logic programming … is based upon the following thesis: predicate logic (calculus) is a useful language for representing knowledge.

– Prolog by Example, page 12

(What do you mean by “useful” language?)

Logic programming style is achieved in full by taking into account Kowalski’s equation (the main thesis of logic programming):

Algorithm = Logic (specifications) + Control (declarations of logical commitment)

– Prolog by Example, page 16

Questions

What is Emscripten?

How to build and run a program with Docker?

Software transactional memory.

Polymorphic variants (in Ocaml).

What is it that makes Coq a proof assistant? What would you have to add to a functional programming language?

What can you do in a dependently-typed language that you can’t in a normal FP language? What properties can’t a dependently-typed language type-check at compile time? I’m guessing that halting won’t be covered, which would mean that all programs would have to terminate.

What are refined types? Liquid Haskell?

What is proof-carrying code?

What are linear types? Apparently variables are used exactly once.

Does Scala have dependent types?

What is the use of holes?