Computer Science
  • All Programming Languages Should Have Linear Types

    by Vanessa McHale | Computer Science

    Much like all dynamically typed languages are poor statically typed languages, typed functional programming languages (corresponding to intuitionistic logic) are subsumed by linear logic. Girard articulates this unity in the logical context. Let us gloss the functional programming side of things.

  • Linear Types for Manipulating Expressions in the Lambda Calculus

    by Vanessa McHale | Computer Science

    If we wish to preserve global uniqueness of names during \(\beta\)-reduction, we have to \(\alpha\)-rename before each substitution. Consider:

  • Linear Effects Handling

    by Vanessa McHale | Computer Science

    Haskell puts all side effects in the IO monad, which passes around the RealWorld. This is unsatisfactory for a number of reasons, and Haskellers have spilled much ink on effects systems. As I recently noted, there are distinctions in how one handles effects at the logical level: in particular, randomness is different from array writes.

  • C Converges to Intuitionistic Logic

    by Vanessa McHale | Computer Science

    C has a reputation for being a "hacker" language, in contrast to say Haskell, which is abstract with ties to logic and category theory. There is even the quip "C is a portable assembler".

  • Logic Programming Doesn't Work in the Real World

    by Vanessa McHale | Computer Science

    Logic programming fails for many reasons; interestingly it fails to integrate with imperative programming or export its constructs. Haskell's monadic I/O—explicitly passing a RealWorld—offers a nice demonstration.