Hirrolot

data Fmt = FArg Fmt | FChar Char Fmt | FEnd

toFmt : (fmt : List Char) -> Fmt
toFmt ('*' :: xs) = FArg (toFmt xs)
toFmt (  x :: xs) = FChar x (toFmt xs)
toFmt [] = FEnd

PrintfType : (fmt : Fmt) -> Type
PrintfType (FArg fmt) = ({ty : Type} -> Show ty => (obj : ty) -> PrintfType fmt)
PrintfType (FChar _ fmt) = PrintfType fmt

Hirrolot

An error occurred:
/tmp/playground3425286633/play.zig:9:9: error: error is ignored. consider using `try`, `catch`, or `if`
        switch (c) {
        ^
/tmp/playground3425286633/play.zig:23:15: note: called from here
    try printf("Mr. John has * contacts in *\n", .{ 42, "New York"});
              ^
/tmp/playground3425286633/play.zig:22:21: note: called from here
pub fn main() !void {
                    ^

Hirrolot

const std = @import("std");

fn printf(comptime fmt: []const u8, args: anytype) anyerror!void {
    const stdout = std.io.getStdOut().writer();

    comptime var arg_idx: usize = 0;

    inline for (fmt) |c| {
        if (c == '*') {
            try printArg(stdout, args[arg_idx]);

Hirrolot

(* The syntax of our calculus. Notice that types are represented in the same way
   as terms, which is the essence of CoC. *)
type term =
  | Var of string
  | Appl of term * term
  | Binder of binder * string * term * term
  | Star
  | Box

and binder = Lam | Pi

Hirrolot

trait Interp {
    type Repr<T>;

    fn lit(i: i32) -> Self::Repr<i32>;
    fn add(a: Self::Repr<i32>, b: Self::Repr<i32>) -> Self::Repr<i32>;
}

struct Eval;

impl Interp for Eval {

Hirrolot

let rec eval = function
  | `Appl (m, n) -> (
      let n' = eval n in
      match eval m with `Lam f -> eval (f n') | m' -> `Appl (m', n'))
  | (`Lam _ | `Var _) as t -> t

let sprintf = Printf.sprintf

(* Print a given term using De Bruijn levels. *)
let rec pp lvl = function

Hirrolot

let lam f = f
let appl f x = f x

Hirrolot

module type Form = sig
  type 'a meaning

  val lam : ('a meaning -> 'b meaning) -> ('a -> 'b) meaning
  val appl : ('a -> 'b) meaning -> 'a meaning -> 'b meaning
end

(* Evaluate a given term. *)
module Eval = struct
  type 'a meaning = 'a

Hirrolot

module type Form = sig
  type ('env, 'a) meaning

  val vz : ('a * 'env, 'a) meaning
  val vs : ('env, 'a) meaning -> ('b * 'env, 'a) meaning
  val lam : ('a * 'env, 'b) meaning -> ('env, 'a -> 'b) meaning

  val appl :
    ('env, 'a -> 'b) meaning -> ('env, 'a) meaning -> ('env, 'b) meaning
end

Hirrolot

type term = Lam of (term -> term) | Appl of term * term | FreeVar of int

let unfurl lvl f = f (FreeVar lvl)
let unfurl2 lvl (f, g) = (unfurl lvl f, unfurl lvl g)

let rec print lvl =
  let plunge f = print (lvl + 1) (unfurl lvl f) in
  function
  | Lam f -> "(λ" ^ plunge f ^ ")"
  | Appl (m, n) -> "(" ^ print lvl m ^ " " ^ print lvl n ^ ")"