Max Heiber 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 = |

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 =

	// 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>

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

	sig AbstractClass, ConcreteClass extends Class {}

	sig MethodName {}

	abstract sig Method {

	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


	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 = [])


	(* 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)

	#!/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

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

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

	hole_is_a_variable()

	Max Heiber
	I'm implementing IDE support for a language using Language Server Protocol.

	I want to trigger a rename after extracting a variable into the current scope. That is, I've implemented steps 1 to 2 of the current flow and want to know how to implement 3 and 4

	1. When the user selects an expression a yellow lightbulb shows up. Example: `z = 3 + /selection-start/5000/selection-end/`
	2. When the user selects "extract into variable" then a new variable called "placeholder" is created in the current scope and the original expression is assigned to it. Example: `placeholder = 5000; z = 3 + placeholder`


	3. The first instance of `placeholder` is highlighted and the text box for renaming pops up. When the user types "the_new_name" and presses `Return` then the text is: `the_new_name = 5000; z = 3 + the_new_name`