ekzhang

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

neel-krishnaswami

module C : sig
  type t 
  val empty : t 
  val one : char -> t 
  val union : t -> t -> t 
  val inter : t -> t -> t 
  val top : t 
  val mem : char -> t -> bool 
  val make : (char -> bool) -> t 
  val equal : t -> t -> bool

bishabosha

//> using scala "3.3.0"

import scala.util.boundary, boundary.break

object Loops:

  type ExitToken = Unit { type Exit }
  type ContinueToken = Unit { type Continue }

  type Exit = boundary.Label[ExitToken]

aradarbel10

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use list comprehension" #-}

import Data.IORef ( IORef, newIORef, readIORef, writeIORef )
import GHC.IO ( unsafePerformIO )
import Control.Applicative ( Alternative(..) )
import Control.Monad ( when )
import Debug.Trace

aradarbel10

(* language definition *)
type nom = string
type bop = Add | Sub | Mul

type typ =
| Int | Arrow of typ * typ | Meta of meta
and meta = meta_state ref
and meta_state =
| Solved of typ
| Unsolved of nom (* keep name for pretty printing *)

AndrasKovacs

{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}

{-|
Minimal dependent lambda caluclus with:
  - HOAS-only representation
  - Lossless printing
  - Bidirectional checking
  - Efficient evaluation & conversion checking

Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196

AndrasKovacs

{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}

{-
Challenge:
- Define a deeply embedded faithfully represented syntax of a dependently typed
  TT in Agda.
- Use an Agda fragment which has canonicity. This means that the combination of
  indexed inductive types & cubical equality is not allowed!
- Prove consistency.

zehnpaard

module D = Effect.Deep

type 'a expr = ..
type _ Effect.t += Extension : 'a expr -> 'a Effect.t

(* Base Interpreter *)
type 'a expr +=
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| Sub : int expr * int expr -> int expr

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