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"

parente

Summary

IPython's display() function can return a DisplayHandle object. You can use a DisplayHandle to update the output of one cell from any other cell in a Jupyter Notebook.

Example

The display_handle.ipynb notebook below calls display(display_id=True) to get a display handle instance. It then uses the DisplayHandle.display method to show some initial, static Markdown. Later, in a different cell, it calls DisplayHandle.update in a loop to show a range of emoji characters.

kseo

#! /usr/bin/env ocamlscript
Ocaml.ocamlflags := ["-thread"];
Ocaml.packs := [ "core" ]
--
open Core.Std

type term =
  | Ident of string
  | Lambda of string * term
  | Apply of term * term

minrk