Computer Science
  • 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.

  • The Moral Imperative to Type Imperative Languages With Linear Logic

    by Vanessa McHale | Computer Science

    "Linear Types can change the world." Lafont has shown us how to create a linear abstract machine. Yet the moral imperative to use linear types in computer science is not widely appreciated.