Programming_Language

Terminologies

Fully qualified name

  • In computer programming, a fully qualified name is an unambiguous name that specifies which object, function, or variable a call refers to without regard to the context of the call.

Encapsulation

Total Function

  1. Every function must be a total (as opposed to partial) function. That is, it must have a definition for everything inside its domain.
  2. A restricted form of recursion, which operates only upon 'reduced' forms of its arguments, such as Walther recursion, substructural recursion, or "strongly normalizing" as proven by abstract interpretation of code.
  3. No effects?

Curry–Howard Correspondence

Currying

  • Currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument

    • The idea actually appears in the Begriffsschrift of Gottlob Frege, published in 1879.
  • Function arrows associate to the right and application associates to the left

    • ℕ → ℕ → ℕ stands for ℕ → (ℕ → ℕ)
    • _+_ 2 3 stands for (_+_ 2) 3

Congruence

  • A relation is said to be a congruence for a given function if it is preserved by applying that function. If e is evidence that x ≡ y, then cong f e is evidence that f x ≡ f y, for any function f.

Gradual Type

Effect Handlers

Floyd-Hoare logic

Separation Logic

First-order Logic