mheiber

Lego Mindset vs. Woordworking Mindset by Scott Stevenson:

• main concepts:
  • legibility (Lego), for which S. Stevenson links to A Big Little Idea Called Legibility (Venkatesh Rao) (oddly, calls that blog post a “seminal work” when it’s just a summary of “Seeing Like a State” by James Scott)
    • S. Stevenson misattributes the forest analogy to Venkatesh Rao! That’s analogy from the first few chapters of Seeing Like a State, so it seems S. Stevenson isn’t familiar with Seeing Like a State and may not have gone too deep on Rao’s summary.
  • the alternative S Stevenson gives to legible (Lego in his analogy) work is “object-level” work (woodworking) which is focused on an outcome (note: this part is very different from Seeing Like a State, where actually the legible solutions are more focused on outcomes!)
• claims:
  • (attempts to justify, but it’s a we

mheiber

Computing with excluded middle, like in Griffin's "A Formulae As Types Notion of Control"

Translated to OCaml using the double-negation translation of classical to intuitionist logic.

type void = |

mheiber

Comparing Coeffects and Effects+Handlers

This document assumes you know what effects+handlers and continuations are. https://effekt-lang.org/docs/concepts/effect-handlers has an interactive introduction and https://ocaml.org/manual/5.2/effects.html has in-depth OCaml examples.

Examples

One use case for coeffects is in implementing implicit parameters. The following example prints 201 in the playground at Coeffects: Context-aware programming languages:

let plus_implicit =

mheiber

// We prove this theorem: forall A,B,C.   A \/ B -> C <-> (A -> C) /\ (B -> C)
// by representing the theorem as a type and showing the type is inhabited.
// To show type inhabitation, we make a value of the type.
// Note: this proof actually demonstrates something practical in programming:
// part of why the visitor pattern can be helpful in OO languages that don't have
// much support for sum types ("or"/algebraic data types) but do have product types ("and"/records).
// https://cs.stackexchange.com/questions/139003/is-there-a-relationship-between-visitor-pattern-and-demorgans-law
type Theorem<A, B, C> = Iff<
                ((either: Or<A, B>) => C),
                And<(a: A) => C, (b: B) => C>

mheiber

abstract sig Class {
   methods: set Method,
   parent: lone Class
}

sig AbstractClass, ConcreteClass extends Class {}

sig MethodName {}

abstract sig Method {

mheiber

Warning: we are not using the native binary ocamlc.opt because it is older than the bytecode binary boot/ocamlc; you should silence this warning by either removing ocamlc.opt or rebuilding it (or `touch`-ing it) if you want it used.
../../ocamlc.opt -nostdlib -I ../../stdlib ../../compilerlibs/ocamlcommon.cma \
	  -I ../../parsing -I ../../driver \
	  cross_reference_checker.ml -o cross-reference-checker
/Library/Developer/CommandLineTools/usr/bin/make -C src all
/Library/Developer/CommandLineTools/usr/bin/make html
../../runtime/ocamlrun ../tools/texquote2 < allfiles.etex > allfiles.texquote_error.tex
mv allfiles.texquote_error.tex allfiles.tex
../../runtime/ocamlrun ../tools/texquote2 < foreword.etex > foreword.texquote_error.tex
mv foreword.texquote_error.tex foreword.tex

mheiber

ocaml_binary(name = 'ackermann_3_2_is_' +
    str(
        (lambda x, m, n: x(x, m, n))
        ((lambda x, m, n: n + 1 if m == 0 else (x(x, m - 1, 1) if n == 0 else x(x, m - 1, x(x, m, n - 1)))), 3, 2)
    ), srcs = [], deps = [])

mheiber

(* from https://okmij.org/ftp/ML/first-class-modules/ *)
module Eq = struct
  type ('a,'b) eq = Refl of 'a option ref * 'b option ref

  let refl () = let r = ref None in Refl (r,r)

  let symm : ('a,'b) eq -> ('b,'a) eq = function 
      Refl (x,y) -> Refl (y,x)

mheiber

#!/usr/bin/env ocaml

module type HdArg = sig
    type t
    val x: t list
    val continuation : t -> unit
end

let hd (module M : HdArg): unit =
    let fn : M.t list -> M.t = function

mheiber

def hole_is_a_variable():
    _ = 'hello'
    print(_) # 'hello'

def hole_is_not_a_variable():
    match 'hello':
        case _:
            print(_) # NameError

hole_is_a_variable()