gbaz

module Lambda where
import qualified Data.Map as M
import Data.Maybe
import Control.Monad.State.Strict
import Debug.Trace

data Term = Lam String Term
          | Var String
          | App Term Term
          | KonstInt Int

gbaz

This post will discuss how to model Simplicial Sets (sSets) in Haskell, using their category-theoretic definition.

Introduction

If you want to know what these are, a good primer is Friedman's introduction to simplicial sets. Another, more concrete perspective is provided by Sergeraert's introduction to combinatorial homotopy theory

Now why would we want to model this thing anyway, and why are we going to jump through categorical hoops to do so?

Well, we want to model sSets because they are a basic way in which people carry out homotopy theory, which in turn is about reducing the class of spaces (or shapes, if you prefer) into spaces modulo their continuous transformations into one another, thus giving us a way to talk about shapes/spaces ""in general"". Now in turn we need to represent shapes/spaces in a concrete way, and we do so by identifying them with certain decompositions of them

gbaz

;; Logical MESS (Logical Martin-Lof Extensible Simulater and Specification)
;; Gershom Bazerman, 2015

(load "interp-uber.scm")
(load "mk/test-check.scm")
(load "mk/matche.scm")

(define ans  (run 1 (q) (evalo
     `(letrec (
	 (reduce (lambda (cxt body)

gbaz

module Generic where

import Prelude
import Data.Maybe
import Data.Traversable
import Data.Array

data GenericSpine = SProd String (Array (Unit -> GenericSpine))
                  | SRecord (Array {recLabel :: String, recValue :: Unit -> GenericSpine})
                  | SNumber Number