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

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

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

RiscInside

-- One argument operations with strict evaluation strategy
inductive UnOp : Type :=
  | ufst                                     : UnOp -- first element of the pair
  | usnd                                     : UnOp -- second element of the pair
  | umkl                                     : UnOp -- left constructor of either type
  | umkr                                     : UnOp -- right constructor of either type
  deriving DecidableEq

open UnOp

AndrasKovacs

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

aradarbel10

{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}

{-
  (compiled with GHC 9.4.2)
-}

{-
  HEADS UP
  this is an example implementation of a non-trivial type system using bidirectional type checking.
  it is...

bramus

🚚 The bookmarklet has moved to https://github.com/bramus/mastodon-profile-redirect/

AndrasKovacs

{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

    "A simple and efficient implementation of strong call by need by an abstract machine"
    https://dl.acm.org/doi/10.1145/3549822

This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.

aradarbel10

%{
(** the [Surface] module contains our AST. *)
open Surface

(** exception raised when a [nonempty_list] returns an empty list. *)
exception EmptyUnfolding

(** desugars `(x y z : a) -> b` into `(x : a) -> (y : a) -> (z : a) -> b`. *)
let rec unfoldPi (xs : string list) (dom : expr) (cod : expr) : expr =
  match xs with

TOTBWF

(** Core Types *)
module Syntax =
struct
  type t =
    | Local of int
    | Hole of string
    | Let of string * t * t
    | Lam of string * t
    | Ap of t * t
    | Pair of t * t