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 racket
(require syntax/parse/define "foods.rkt" (for-syntax "foods.rkt"))

(add-delicious-food! "pineapple")
(add-delicious-food! "sushi")
(add-delicious-food! "cheesecake")

(define-simple-macro (add-food-combinations! [fst:string ...]
                                             [snd:string ...])
  #:do [(for* ([fst-str (in-list (syntax->datum #'[fst ...]))]

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

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

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

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

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)