András Kovács AndrasKovacs

Comparing GHC Core for Parsley and flatparse for a simple s-expression parser. GHC 8.6.6, flatparse 0.5.2.1, parsley 2.0.0.1

Flatparse source:

{-# language TemplateHaskell #-}

module FP (runSexp) where

import FlatParse.Basic

Lightweight region memory management in a two-stage language

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

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.

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


	{-# language Strict, LambdaCase #-}

	module ReasonableLC where

	type Ix = Int
	type Lvl = Int

	-- environment trimming, drops some entries
	data Trim = Empty \| Keep Trim \| Drop Trim

	{-
	Conor McBride's "classy hack" for getting HOAS notation for FOAS: https://mazzo.li/epilogue/index.html%3Fp=773.html
	The following is a code-golfed version where we observe that by sprinkling some singletons
	in the standard FOAS definition of terms, we get an equivalent definition (because singletons are
	contractible) which supports HOAS notation directly.
	-}

	{-# OPTIONS --backtracking-instance-search #-}

	open import Relation.Binary.PropositionalEquality


	{-# language DeriveFunctor, DeriveFoldable, RankNTypes, LambdaCase #-}

	-- -- Breadth first

	-- import Control.Applicative
	-- import Control.Monad

	-- data Tree a = Zero \| One a \| Node (Tree a) (Tree a)



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

	{-# 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

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