lexi-lambda

Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation m >>= f, then f is m’s continuation. It’s the function that is called with m’s result to continue execution after m returns.

If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have

m >>= f >>= g >>= h

then the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.

lexi-lambda

#lang typed/racket/base

(require (for-syntax racket/base
                     racket/sequence
                     racket/syntax
                     syntax/parse
                     syntax/stx)
         racket/match)

(begin-for-syntax

lexi-lambda

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Language.HigherRank.Main
  ( Expr(..)
  , EVar(..)
  , Type(..)
  , TVar(..)
  , TEVar(..)
  , runInfer
  ) where

lexi-lambda

With scoped effects, handlers must be a part of the program

It is seductive to imagine that effect handlers in an algebraic effect system are not part of the program itself but metalanguage-level folds over the program tree. And in traditional free-like formulations, this is in fact the case. The Eff monad represents the program tree, which has only two cases:

data Eff effs a where
  Pure :: a -> Eff effs a
  Op :: Op effs a -> (a -> Eff effs b) -> Eff effs b

data Op effs a where

lexi-lambda

KSSU splits timer GUI challenge

This document presents an informal “GUI framework benchmark” along the lines of [TodoMVC][]: it is a relatively simple, well-defined problem that can be used to illustrate the strengths and weaknesses of different GUI paradigms. However, unlike TodoMVC, this problem is specifically designed to stress test state management in multi-stage modal flows, where modifications to the application state can be complex but must not be committed immediately.

The problem in question is to write a speedrunning timer for [Kirby Super Star Ultra][kssu]’s [True Arena boss rush mode][kssu-true-arena]. This is a completely meaningless problem to most people, but that’s okay—this document does not assume any familiarity with KSSU or with speedrunning timers more generally. However, I do want to go over a couple basics to provide some context on the problem being solved:

• The True Arena is a videogame boss rush mode where the objective is to beat a series of bosses as quickly as possible.

lexi-lambda

#lang racket

(require (for-syntax racket/function
                     syntax/apply-transformer)
         syntax/parse/define)

(define-syntax ($expand stx)
  (raise-syntax-error #f "illegal outside an ‘expand-inside’ form" stx))

(begin-for-syntax

lexi-lambda

#lang racket/base

(require (for-meta 2 racket/base
                     syntax/parse)
         (for-syntax racket/base
                     racket/list
                     racket/trace
                     syntax/kerncase
                     threading)
         racket/sequence

lexi-lambda

{-# LANGUAGE FlexibleInstances #-}

-- | An implementation of Section 3, Local Type Argument Synthesis, from the
-- paper /Local Type Inference/ by Pierce and Turner.
module Infer where

import Control.Monad (foldM, join, zipWithM)
import Data.Function (on)
import Data.List (foldl', groupBy, intercalate, intersect, nub)

lexi-lambda

module Matrix where

open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.List as List using (List; []; _∷_; product)
open import Data.Nat as Nat
open import Data.Nat.Properties as Nat
open import Data.Product as Prod
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

lexi-lambda

Racket #langs and the REPL

The Racket platform provides a robust set of tools for developing languages, mostly centered around the macro system and the #lang protocol, which allows providing arbitrary readers to convert text input to syntax objects representing Racket modules. The REPL is a bit more complicated, however, because it has different rules—each expression needs to be dynamically read, assigned lexical context, expanded, compiled, evaluated, and printed, all in real time. (In that sense, perhaps the phrase “REPL” oversimplifies what Racket is doing, but that’s a separate conversation.)

So how does Racket accommodate this in the face of completely arbitrary user-defined languages, some of which may not even support interactive evaluation in a traditional sense? Racket mostly solves this problem by having a related but distinct set of protocols for managing runtime interactions that operates alongside #lang.

Modules and the top level

Racket’s evaluation model divides pretty much ev