AndrasKovacs

Lightweight region memory management in a two-stage language

• Intro
• Basics
  • Stage inference
• Regions
  • Bit-stealing
  • Using regions
• Eager regions

AndrasKovacs

Basic setup for formalizing elaboration

First attempts

Elaboration is, broadly speaking, taking user-written syntax and converting it to "core" syntax by filling in missing information and at the same time validating that the input is well-formed.

I haven't been fully happy with formalizations that I previously used, so I make a new attempt here. I focus on a minimal dependently typed case.

AndrasKovacs

{-# language
    BlockArguments
  , CPP
  , LambdaCase
  , MagicHash
  , PatternSynonyms
  , Strict
  , TypeApplications

AndrasKovacs

{-# OPTIONS --without-K #-}

-- version 1, conversion is indexed over conversion
module IndexedConv where

  data Con  : Set
  data Ty   : Con → Set
  data Sub  : Con → Con → Set
  data Tm   : ∀ Γ → Ty Γ → Set
  data Con~ : Con → Con → Set

AndrasKovacs

{-# language
  BlockArguments
, ConstraintKinds
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}

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

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.

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.

AndrasKovacs

-- Examples

data Foo = A | B | C

foo :: Foo -> Int
foo A = 10
foo B
foo C = 20

foo :: Foo -> Int