Contents

Blog tags RSS

Entries tagged programming

Stack reification via trampolines

21 February 2016 (programming language java)

I've been spending a couple weeks now on getting Időrégész to Android in the best possible way. Időrégész is the Hungarian text adventure game from the '80s that I reverse-engineered and then re-implemented in Inform. My original plan was to just implement a Glulx interpreter; however, initial experiments with a Clojure implementation weren't too promising on the performance front.

I decided to turn to compilation instead of interpretation, then: take the Inform-emitted Glulx image, and compile that directly to the JVM. Of course, that approach would have its own problems with self-modifying code, but my goal is just to get it working well enough that I can compile Időrégész, which is very vanilla as far as Inform programs go.

Most instructions of Glulx map to JVM instructions in a relatively straightforward manner; some unsigned integer operations are implemented by hand in Java and then called via invokestatic. The rather baroque string compression is currently handled at compile time, by just emitting a single Java function that looks like this:

public String resolveString(int ptr)
{
  switch (ptr) {
    case 32851 : return "Class" ;
    case 32857 : return "Object" ;
    case 32863 : return "Routine" ;
    // and so on...
}
    

However, there is one aspect of Glulx that makes the compilation trickier than a straightforward mapping of procedures to procedures and calls to calls: some Glulx opcodes provide fairly detailed access to the runtime state. For example, save must be able to serialize enough of the state that it can later load that back and continue with the next instruction.

In an interpreter, this is a trival matter, since things like the VM's memory and the stack are already reified data structures. However, if it's compiled to JVM, the state of the Glulx program and the state of the JVM is one and the same; so how do you then save it — from the inside?

The solution is to not use the JVM's stack as the Glulx stack; rather, function calls are compiled to areturn instructions that return a small Java object describing which function to call and where to jump back once its result is available. Returns are also compiled to areturn instructions, but this time returning an object describing the result value. Function-local variables and the per-function stack are passed to the generated JVM code as function arguments:

Each Glulx function is compiled into a class that extends the Glulx.Fun class, defined in Kotlin as:

package Glulx

abstract class Fun {
  abstract class Cont {
    class Return(val value : Int) : Cont()
    class Call(val args: IntArray, val nextFun : Fun, val contPC : Short) : Cont()
  }

  class Result(val value : Int, val contPC : Short)

  abstract fun enter(stub: Stack.CallStub?, args: IntArray): Stack.CallFrame
  abstract fun exec(result: Result?, localVars: IntArray): Cont
}
    

Since the JVM doesn't support computed jumps, the continuation address contPC is handled by starting the exec of each Fun with a big tableswitch. Here's an example of a recursively defined factorial function (using the Krakatau JVM assembler's syntax):

.method public exec : (LGlulx/Fun$Result;[I)LGlulx/Fun$Cont;
  .code stack 10 locals 10
    aload_1
    ifnull LSTART

    aload_1
    invokevirtual Method Glulx/Fun$Result getContPC ()S
    tableswitch 0
      LCONT0
      default: LSTART

  LSTART:
    ;; if V0=0, jump to base case
    aload_2
    ldc 0
    iaload

    ifeq L0

    ;; START call FACT(V0-1)
    ldc 1
    newarray int
    dup
    ldc 0
    aload_2
    ldc 0
    iaload
    ldc 1
    isub
    iastore

    new Glulx/Fun$Cont$Call
    swap
    dup2
    getstatic Field Glulx/Image/FACT fun LGlulx/Fun;
    ldc 0
    invokespecial Method Glulx/Fun$Cont$Call <init> ([ILGlulx/Fun;S)V
    pop
    areturn

  LCONT0:
    aload_1
    invokevirtual Method Glulx/Fun$Result getValue ()I
    ;; END call FACT(V0-1)
    ;; Note the code generated for the call spans an areturn!

    ;; Multiply result by V0
    aload_2
    ldc 0
    iaload
    imul

    ;; Return result -- this is the "real" return
    new Glulx/Fun$Cont$Return    
    swap
    dup2
    invokespecial Method Glulx/Fun$Cont$Return <init> (I)V
    pop
    areturn

  L0:
    ;; For the base case, we just return 1
    new Glulx/Fun$Cont$Return
    dup
    ldc 1
    invokespecial Method Glulx/Fun$Cont$Return <init> (I)V
    areturn
  .end code
.end method
    

Running these functions then becomes a matter of mere stack juggling, implemented again in Kotlin:

package Glulx

class Stack {
  class CallFrame(val parent: CallStub?, val localVars: IntArray) {
    constructor(parent: CallStub?, localVarCount: Int):
      this(parent, IntArray(localVarCount))
        
    fun storeArgs(args: IntArray) {
      for(i in args.zip(localVars).indices)
        localVars[i] = args[i]
    }
  }
  
  class CallStub(val parent: CallFrame, val parentFun: Fun, val parentPC : Short)
}

fun run(startFun: Fun) {
  var frame = startFun.enter(null, IntArray(0))
  var fn = startFun
  var result : Fun.Result? = null

  while (true) {
    val cont = fn.exec(result, frame.localVars)
    when (cont) {
      is Fun.Cont.Return -> {
         val stub = frame.parent
         if (stub == null) return

         frame = stub.parent
         fn = stub.parentFun
         result = Fun.Result(cont.value, stub.parentPC)
      }
      is Fun.Cont.Call -> {
        val stub = Stack.CallStub(frame, fn, cont.contPC)
        fn = cont.nextFun
        frame = fn.enter(stub, cont.args)
        result = null
      }
    }
  }
}
    

In the real implementation, there's slightly more state to pass around: Fun.exec also gets as argument an instance of a generic Environment class which it can use to e.g. access the main Glulx memory, or to issue Glk calls; and there are some boring details about handling both 32-, 16- and 8-bit local variables.

Note that the exact same technique can also be used to implement tail recursion (even mutual tail recursion) on a platform that doesn't support it, like the JVM. I am not using it here, but Glulx actually has a tailcall instruction (not used by Időrégész, or sane Inform code in general), so it might come handy if I want to increase feature coverage.

Hacks of 2015

28 December 2015 (programming haskell idris games electronics fpga meta)

Encsé writes in his blog that one of the reasons he created a tiny CPS-based Scheme interpreter was because he realized he hasn't done any fun side projects all year. So I thought I'd make an inventory of fun hacks I've done in 2015.

Bit-fiddling

Games

Talks

Functional programming

Stack Overflow highlights

Some of the answers I wrote this year on Stack Overflow required me to learn just enough of something new to be able to answer the question:

Then, there were those where it turned out there was a bug to be found by scratching the surface of the question deep enough:

Then there were the answers that were just too much fun to write:

All in all, it seems this has been quite a productive year for me out of the office, even if you exclude the Stack Overflow part. I was actually surprised how long this list was while compiling it for this blog post. Maybe I should write a list like this every year from now...

Időrégész 2015

5 June 2015 (programming retro games)

Amikor már megvolt a C64-ünk, megkaptam egyszerre az LSI-féle 1001 játék sorozat első három részét anyukáméktól (ez úgy '89 körül lehetett), azt hiszem a negyedik-ötödik rész később jelent meg. Annyira nem voltam a scene-ben, hogy azt sem tudtam, hogy van olyan, hogy scene. Az én scene-em az a pár általános iskolai osztálytárs volt, akinek legalább egy ZX Spectrumja volt. Szóval a lényeg, hogy ez a pár könyv volt minden kapcsolatom a C64 játékokkal. Azon a néhány játékon kívül, amik így apukám ismerősein keresztül jutottak hozzánk, a többiről csak olvasni tudtam. Persze a leírás alapján mindegyik a legjobb játéknak tűnt EVER!, és volt néhány, amit el is kezdtem BASIC-ben leprogramozni az alapján, ahogy elképzeltem; ez nyilván több oldalról is ab ovo teljes sikertelenségre volt ítélve.

A harmadik 1001 játékban volt egy végigjátszás az Időrégészről, amibe persze azonnal beleszerettem. A szöveges kalandjáték volt az egyetlen játék-műfaj, aminek a programozásában akkortájt labdába tudtam rúgni annyira, hogy valami játszható jöjjön ki belőle, és emiatt pláne úgy éreztem, hogy ez a játék megszólít engem. Ráadásul nem is tudom, hogy volt-e akkor már CoV, de az biztos, hogy én nem ismertem (a Magic Candle-ös szám volt az első, amikor belefutottam, ha minden igaz, '92-ben), úgyhogy a leírás stílusa, humora is egy teljesen új világot nyitott meg előttem.

Mivel a fent ecsetelt okok miatt warez-ként esélyem se volt hozzájutni, ez lett a második játék, amit eredetiben megvettünk (az első az Impossible Mission 2 volt (kazettán), de azzal én nem sokat játszottam, azt apukám tolta — külön post lehetne, amikor az éjszaka közepén, a TV hangerejét éppen csak hallhatóra állítva ordított a figura leesés közben).

A játék csalódást nem okozott, de végigjátszani az istennek se ment, még az 1001-leírás alapján sem. Az áttörést csak 1991-ben hozta egy osztálytársam, aki rájött, hogy SPOILER ALERT a papnál még imádkozni is kell, nem elég odaadni neki az aranykeresztet vagy mit.

Most illene arról is írni, hogy akkor most ez egy jó játék volt-e. Azt gondolom, hogy most tudom a legkevésbé ezt megítélni, mert túl közelről látom (mint majd mindjárt kiderül hogy miért). Az biztos, hogy akinek annak idején volt C64-e (vagy akár +4-e!), és magyar, az ismeri az Időrégészt meg a többi Rátkai-játékot: nem véletlenül volt róla IDDQD cikk meg Index illetve Facebook csoportok. Igazi cult classic.

Egy modern Időrégész-reprodukció terve

Mostanában elkezdtek érdekelni a régi 8-bites gépek, mivel annak idején az alacsonyszintű programozásuk, meg úgy egyáltalán a felépítésük totál kimaradt nekem. Most, hogy autodidakta módon FPGA-fejlesztést tanulok, elértem oda, hogy épkézláb számítógépeket tudok építeni, amihez persze elkerülhetetlen, hogy megismerjem minden kis részletüket. Ennek egyébként egy nem várt, de kellemes mellékhatása, hogy tudom értékelni a korabeli és azóta készült demókat, amikor minden képkockát önmagában is lehetetlennek tűnik előállítani a C64-en.

Szóval kitaláltam, hogy kipróbálnám egy játék teljes visszafejtését, mivel ilyesmit sose csináltam még. Egy ilyen nem-realtime, nem-grafikus játék, mint az Időrégész, remek kezdő projektnek tűnt. Az alap-elképzelés (még május elején) az volt, hogy visszafejtem a programot annyira, hogy tudjam minden részéről hogy mit csinál, és ezalapján megértem, és minél magasabb szinten reprodukálom a működését. Hogy valami igazán örök formában rögzítsem, mindenképpen a ZMachine virtuális gépet terveztem célbavenni, mivel a modern interactive fiction-világban ez tűnik egyértelműen a bevett eszköznek már évtizedek óta.

Continue reading »

Initial version of my Commodore PET

2 March 2015 (programming haskell FPGA electronics retro)

In my quest to build more and more complicated computers on FPGAs armed with nothing but a crappy hobbist mindset and some hazy ideas of how Kansas Lava is supposed to work, I've reached another milestone: my first real computer.

That is, unlike the Brainfuck CPU that I designed myself, or the CHIP-8, which was originally a virtual machine spec (with all the implementation leeway that implies), this latest subject is a bona fide 8-bit home computer from the seventies: the Commodore PET.

A Commodore PET 2001 from 1977

The Commodore PET in a nutshell

The PET is a very simple machine compared to later Commodore models, which is why I thought it would make a good first step on a journey that I hope will one day culminate in implementing a Commodore 64. Its centerpiece is the MOS 6502 CPU (practically the same as the MOS 6510 used in the C=64), and there are only four other components: a text-only video signal generator and three IO interface chips (two PIA's and one VIA) for keyboard, Datasette and extension port communication. Just hooking up one of the PIAs is enough to get a minimal system working with keyboard input.

12 KBytes of PET ROM contain implementation of basic IO routines (the so-called "kernal"), the full-screen text editor, and Microsoft's BASIC interpreter. Then there's a separate character ROM (not addressable from the CPU) used by the video generator.

MOS 6502

The 6502 microprocessor was a staple of the eight-bit home computer era of the late seventies and eighties. By today's standards, it is incredible to imagine what it must have been like to design it manually, drawing the layout with pencils on paper. On the other hand, if it was designed in such a low-tech way, I figured it shouldn't be too difficult to build something compatible using modern tools even by a hobbist like myself. And of course there are already dozens of home-built 6502 implementations out there, to varying degrees of compatibility.

The ultimate reference on the 6502 must be the Visual 6502 Project which I deliberately avoided consulting. I don't really see the educational value in copying the original 6502 design; so instead, I went with a more black-box approach by just looking at the opcode descriptions and interrupt model and working from that.

The first milestone I aimed for was to get enough of the CPU working that I can run the sample programs on 6502asm.com, which defines a tiny microcomputer-like architecture that doesn't have interrupts or any fancy video modes: you just have 32×32 pixels with a fixed 16-color palette mapped to main RAM from $0200, and a zero page-mapped register for keyboard input that you can do polling on. The Kansas Lava implementation is really simple and I plan to reuse it later if I do a similar project with the Z80.

My workflow was that I would use ca65 to assemble test programs, burn them into ROM, and run it in the Kansas Lava simulator for a couple thousand cycles; then render the video RAM into a GTK+ window. I would start with this program that does nothing but moves data around in memory (drawing the Commodore logo pixel by pixel), and basically I implemented the 6502 opcodes as I went along. After two days of work, I finally got it working:

First positive result

Seeing this was an incredible feeling. The input was valid 6502 machine code, and my very own CPU managed to run it correctly for the approximately 40,000 cycles that it took to draw this image. There was no stopping at this point: I already had a working VGA frame buffer implementation from the CHIP-8, so next day I synthesized it and run it on real hardware, my venerable Papilio Pro:

Hi-tech from the seventies, today!

Simulation-based testing

As I added more and more opcodes and started running more and more complicated programs, things very quickly stopped working. My CPU was full of bugs, and figuring out what went wrong by looking at the simulation logs after running it for tens of thousands of cycles was very tedious.

And so, it was at this point that I started adding unit tests. The framework for writing tests exposes a monad where the available effects are making observations on the state of the system (CPU registers and contents of the memory) and executing instructions. This presents an API that allows writing tests in an imperative way:

php = do
    flags <- observe statusFlags
    sp <- observe regSP
    execute0 0x08
    sp' <- observe regSP
    pushed < observe $ mem (stackAddr <$> sp)
    assertEq "Stack pointer is decremented" sp' (pred <$> sp)
    assertEq "Status is correctly pushed" pushed flags
      

A test like this is turned into a ROM image containing $08 at the address pointed to by the reset vector. The simulation is then run until the CPU enters the Fetch internal state for the second time (the first time is when it fetches the opcode under testing, i.e. the PHP ($08) instruction), and then the observations are evaluated by looking at the simulation output in the same cycles as the Fetch state. Of course, this means you shouldn't be able to write tests like the following:

impossiblyDynamicTest = do
    arg <- observe regX
    execute1 0x00 arg
    a' <- observe regA
    assertEq "A is updated" a' arg
      

This is ensured by observe returning values wrapped in an Obs type, and execute1 requiring unwrapped arguments:

observe :: Query a -> TestM (Obs a)
execute1 :: Byte -> Byte -> TestM ()
assertEq :: (Eq a, Show a) => String -> Obs a -> Obs a -> TestM ()
      

To allow assertions over derived values, Obs is an applicative functor (in fact, it is the free applicative functor over the co-Yoneda functor of the primitive observations).

I think this approach has merit as a general framework for hardware simulator-based unit testing and I intend to extend it and maybe even carve it out into a separate library in the future.

A Minimal Viable PET

Once I had a sufficiently working CPU, I started building the other pieces around it. I took the PET emulator from the VICE suite and commented out all the PIA and VIA code, replacing writes with nops and reads with hardcoded values, until I was able to boot it up with the stock ROM to get to the READY. prompt. Of course, since the PIA supplying the interrupt used for timing was removed by that point, I had no flashing cursor or keyboard input. All in all, the system got to a steady state in about 80,000 operations. (Since my implementation is not yet cyle-accurate, I had to switch to counting operations instead of cycles beyond this point. Every operation is at least as fast as on the real chip, so I hope by adding some wait cycles I'll be able to take care of this at some later point.)

After hooking up the same hardcoded values on the same addresses to the CPU, the next step was running the simulator and peeking at the video memory area ($8000..$8FFF on the PET), using the original fonts to render the screen. The initial version showed there might be someone home (sorry for crap quality on the screenshot):

Yeah...

By comparing detailed logs from running the emulator and the simulator, I was able to make observations like "the first 12,345 steps seem to be in agreement", which was a big boost to productivity, getting me, in short order, to this:

Almost there!

After fixing some more bugs in the arithmetic opcodes, I was finally rewarded by this sight:

Ah... much better.

Adding more components

While working on the CPU, I also started writing the character generator, on top of the VGA signal generator in the kansas-lava-papilio package that I originally made for the CHIP-8. This way, the VGA synchronization signals were abstracted away from me and I just had to take care of pumping out the actual pixels. This turned out to be tricker than I originally thought, since you have to time all read-aheads just right so that everything is at hand just in time for the next pixel. So before it finishes drawing the 8 pixels that make up a single row of a character, the next character index is loaded from RAM, and then the character ROM is consulted for the first row of the font image of the next indexed character. Initial versions were having some ghosting issues, or even more fun, full character transpositions (like showing the character from one line above in the first position of each line).

The Commodore PET diverts the vsync signal from the video generator to one of the PIA chips, which generates a CPU interrupt that can be acknowledged by reading from one of its memory-mapped registers. So the next obvious step was to implement this functionality to get the cursor blinking! This required more than just implementing a PIA, since I didn't even have interrupts in the CPU at that point.

But all that work was totally worth it:

And now, here we are

The current version supports keyboard input from PS/2 keyboards (but not all keys are mapped yet), so for the first time since I started working on this more than a month ago, it can be used to write and run BASIC programs!

What you can't see on the video below is that there's still a bug somewhere that causes the classic 10 PRINT "FOO": 20 GOTO 10 program to terminate with an out of memory error after some time.

Apart from fixing these bugs, the big outstanding feature is to add Datasette support so that programs can be loaded and saved to virtual "casettes". For a first version, I'll just burn some extra ROM onto the FPGA containing the tape images and hook that up to the PIA controlling the casette player; but I guess the proper way to do this would be to use something like an SD card reader to get proper persistent, read-writable storage. Or maybe, alternatively, have some kind of serial-over-USB communication with a computer acting as the Datasette unit.

Typed embedding of STLC into Haskell

5 February 2015 (programming haskell language correctness)

Someone posted to the Haskell subreddit this blogpost of Lennart where he goes step-by-step through implementing an evaluator and type checker for CoC. I don't know why this post from 2007 showed up on Reddit this week, but it's a very good post, pedagogically speaking. Go and read it.

In this post, I'd like to elaborate on the simply-typed lambda calculus part of his blogpost. His typechecker defines the following types for representing STLC types, terms, and environments:

data Type = Base
          | Arrow Type Type
          deriving (Eq, Show)

type Sym = String

data Expr = Var Sym
          | App Expr Expr
          | Lam Sym Type Expr
          deriving (Eq, Show)
      

The signature of the typechecker presented in his post is as follows:

type ErrorMsg = String
type TC a = Either ErrorMsg a
newtype Env = Env [(Sym, Type)] deriving (Show)

tCheck :: Env -> Expr -> TC Type
      

My approach is to instead create a representation of terms of STLC in such a way that only well-scoped, well-typed terms can be represented. So let's turn on a couple of heavy-weight language extensions from GHC 7.8 (we'll see how each of them is used), and define a typed representation of STLC terms:

{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-} -- sigh...

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Equality

-- | A (typed) variable is an index into a context of types
data TVar (ts :: [Type]) (a :: Type) where
    Here :: TVar (t ': ts) t
    There :: TVar ts a -> TVar (t ': ts) a
deriving instance Show (TVar ctx a)

-- | Typed representation of STLC: well-scoped and well-typed by construction
data TTerm (ctx :: [Type]) (a :: Type) where
    TConst :: TTerm ctx Base
    TVar :: TVar ctx a -> TTerm ctx a
    TLam :: TTerm (a ': ctx) b -> TTerm ctx (Arrow a b)
    TApp :: TTerm ctx (Arrow a b) -> TTerm ctx a -> TTerm ctx b
deriving instance Show (TTerm ctx a)
      

The idea is to represent the context of a term as a list of types of variables in scope, and index into that list, de Bruijn-style, to refer to variables. This indexing operation maintains the necessary connection between the pointer and the type that it points to. Note the type of the TLam constructor, where we extend the context at the front for the inductive step.

To give a taste of how convenient it is to work with this representation programmatically, here's a total evaluator:

-- | Interpretation (semantics) of our types
type family Interp (t :: Type) where
    Interp Base = ()
    Interp (Arrow t1 t2) = Interp t1 -> Interp t2

-- | An environment gives the value of all variables in scope in a given context
data Env (ts :: [Type]) where
    Nil :: Env '[]
    Cons :: Interp t -> Env ts -> Env (t ': ts)

lookupVar :: TVar ts a -> Env ts -> Interp a
lookupVar Here      (Cons x _)  = x
lookupVar (There v) (Cons _ xs) = lookupVar v xs

-- | Evaluate a term of STLC. This function is total!
eval :: Env ctx -> TTerm ctx a -> Interp a
eval env TConst = ()
eval env (TVar v) = lookupVar v env
eval env (TLam lam) = \x -> eval (Cons x env) lam
eval env (TApp f e) = eval env f $ eval env e
      

Of course, the problem is that this representation is not at all convenient for other purposes. For starters, it is certainly not how we would expect human beings to type in their programs.

My version of the typechecker is such that instead of giving the type of a term (when it is well-typed), it instead transforms the loose representation (Term) into the tight one (TTerm). A Term is well-scoped and well-typed (under some binders) iff there is a TTerm corresponding to it. Let's use singletons to store type information in existential positions:

$(genSingletons [''Type])
$(singDecideInstance ''Type)

-- | Existential version of 'TTerm'
data SomeTerm (ctx :: [Type]) where
    TheTerm :: Sing a -> TTerm ctx a -> SomeTerm ctx

-- | Existential version of 'TVar'
data SomeVar (ctx :: [Type]) where
    TheVar :: Sing a -> TVar ctx a -> SomeVar ctx

-- | A typed binder of variable names
data Binder (ctx :: [Type]) where
    BNil :: Binder '[]
    BCons :: Sym -> Sing t -> Binder ts -> Binder (t ': ts)
      

Armed with these definitions, we can finally define the type inferer. I would argue that it is no more complicated than Lennart's version. In fact, it has the exact same shape, with value-level equality tests replaced with Data.Type.Equality-based checks.

-- | Type inference for STLC
infer :: Binder ctx -> Term -> Maybe (SomeTerm ctx)
infer bs (Var v) = do
    TheVar t v' <- inferVar bs v
    return $ TheTerm t $ TVar v'
infer bs (App f e) = do
    TheTerm (SArrow t0 t) f' <- infer bs f
    TheTerm t0' e' <- infer bs e
    Refl <- testEquality t0 t0'
    return $ TheTerm t $ TApp f' e'
infer bs (Lam v ty e) = case toSing ty of
    SomeSing t0 -> do
        TheTerm t e' <- infer (BCons v t0 bs) e
        return $ TheTerm (SArrow t0 t) $ TLam e'

inferVar :: Binder ctx -> Sym -> Maybe (SomeVar ctx)
inferVar (BCons u t bs) v
  | v == u = return $ TheVar t Here
  | otherwise = do
      TheVar t' v' <- inferVar bs u
      return $ TheVar t' $ There v'
inferVar _ _ = Nothing        
      

Note that pattern matching on Refl in the App case brings in scope type equalities that are crucial to making infer well-typed.

Of course, because of the existential nature of SomeVar, we should provide a typechecker as well which is a much more convenient interface to work with:

-- | Typechecker for STLC
check :: forall ctx a. (SingI a) => Binder ctx -> Term -> Maybe (TTerm ctx a)
check bs e = do
    TheTerm t' e' <- infer bs e
    Refl <- testEquality t t'
    return e'
  where
    t = singByProxy (Proxy :: Proxy a)

-- | Typechecker for closed terms of STLC
check_ :: (SingI a) => Term -> Maybe (TTerm '[] a)
check_ = check BNil        
      

(The SingI a constraint is an unfortunate implementation detail; the kind of a is Type, which is closed, so GHC should be able to know there is always going to be a SingI a instance).

To review, we've written a typed embedding of STLC into Haskell, with a total evaluator and a typechecker, in about 110 lines of code.

If we were doing this in something more like Agda, one possible improvement would be to define a function untype :: TTerm ctx a -> Term and use that to give check basically a type of Binder ctx -> (e :: Term) -> Either ((e' :: TTerm ctx a) -> untype e' == e -> Void) (TTerm ctx a), i.e. to give a proof in the non-well-typed case as well.

Full code as a gist on Github

Older entries:

Entries from all tags