hirrolot

let discard _a b = b

let rec pp lvl = function
  | `Lam f -> "(λ" ^ pp (lvl + 1) (f (`Go lvl)) ^ ")"
  | `Pi (a, f) -> "(Π" ^ pp lvl a ^ "." ^ pp (lvl + 1) (f (`Go lvl)) ^ ")"
  | `Appl (m, n) -> "(" ^ pp lvl m ^ " " ^ pp lvl n ^ ")"
  | `Ann (m, a) -> "(" ^ pp lvl m ^ " : " ^ pp lvl a ^ ")"
  | `Go x -> string_of_int x
  | `Star -> "*"
  | `Box -> "☐"

hirrolot

type term = Call of string * term list

let rec decide_he (s, (Call _ as t)) =
  he_by_diving (s, t) || he_by_coupling (s, t)

and he_by_diving (s, Call (_h', args')) =
  List.exists (fun t -> decide_he (s, t)) args'

and he_by_coupling (Call (h, args), Call (h', args')) =
  if h = h' then List.for_all2 (fun s t -> decide_he (s, t)) args args'

hirrolot

type term = Var of string | Call of string * term array
[@@deriving show { with_path = false }]

type possibilities = term array [@@deriving show]

let demux ~(x : string) ~(values : term array) : term -> possibilities =
  let rec go = function
    | Var y when x = y -> values
    | Var _ as t -> Array.map (fun _ -> t) values
    | Call (op, args) ->

VictorTaelin

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

hirrolot

This is the predecessor of Mazeppa.

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by th

hirrolot

module Make_term (S : sig
  type 'a t [@@deriving show]
end) =
struct
  type t = def S.t

  and def = Lam of t | Var of int | Appl of t * t
  [@@deriving show { with_path = false }]

  let _ = S.show

VictorTaelin

// A nano dependent type-checker featuring inductive types via self encodings.
// All computation rules are justified by interaction combinator semantics,
// resulting in major simplifications and improvements over old Kind-Core.
// Specifically, computable annotations (ANNs) and their counterpart (ANN
// binders) and a new self encoding based on equality (rather than dependent
// motives) greatly reduce code size. A more complete file, including
// superpositions (for optimal unification) is available on the
// Interaction-Type-Theory repository.
// Credits also to Franchu and T6 for insights.

AndrasKovacs

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

jumbojets

type Fun<D, C> = Box<dyn Fn(D) -> C>;

trait Form {
    type Repr<T>;

    fn lam<A, B>(f: Fun<Self::Repr<A>, Self::Repr<B>>) -> Self::Repr<Fun<A, B>>;

    fn appl<A, B>(f: Self::Repr<Fun<A, B>>, x: Self::Repr<A>) -> Self::Repr<B>;
}

hirrolot

This is a minimalistic OCaml implementation of the type system from chapter 30 of TAPL, "Higher-Order Polymorphism".

The implementation uses bidirectional typing and does not feature existential types. Binders are represented as metalanguage functions (HOAS-style); free variables (TyFreeVar & FreeVar) are represented as De Bruijn levels.

See also:

• "Barebones lambda cube in OCaml"
• "How to implement dependent types in 80 lines of code"