Skip to content

Instantly share code, notes, and snippets.

@cheery
cheery / Main.purs
Last active Aug 20, 2020
Record experiments with Paluh
View Main.purs
module Main where
import Prelude
import Effect (Effect)
import Data.Foldable (fold)
import TryPureScript (h1, h2, p, text, list, indent, link, render, code)
import Unsafe.Coerce (unsafeCoerce)
import Prim.RowList
import Prim.Row
@cheery
cheery / TypeFam.hs
Created Jul 28, 2020
Relation that converts between JS values and Haskell values.
View TypeFam.hs
{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}
module TypeFam where
data JsValue = VArray [JsValue] | VNum Double | VString String deriving (Show)
data JsTypeMap
= AsDouble
| AsList JsTypeMap
| AsString
deriving (Show)
View ICat.idr
module ICat2
%default total
data Ft -- functors
= Var Nat
| Terminal
| Prod Ft Ft
| Exp Ft Ft
@cheery
cheery / LC.hs
Created Jun 11, 2020
Concurrently running linearly typed experiment.
View LC.hs
{-# LANGUAGE FlexibleInstances #-}
module LC where
import Control.Monad.Cont
import Control.Monad (guard)
import Control.Concurrent
import Data.Bifunctor (bimap)
-- Interface to retrieve a boolean and then produce a boolean.
interface1 :: FT
@cheery
cheery / Linc.hs
Last active May 30, 2020
Experiment, Optimal reduction with justification (and sausages)
View Linc.hs
module Linc where
import Data.STRef
import Control.Monad.ST
import Control.Monad ((>=>))
data Structure = Structure
{ term :: Tm Int Int
, link_count :: Int
, opt_count :: Int
@cheery
cheery / INet.hs
Created May 27, 2020
"Optimal reduction" implemented with ST monad
View INet.hs
module INet where
import Data.STRef
import Control.Monad.ST
-- This kind of implementation of optimal reduction
-- accumulates control nodes (Croissants and brackets)
--
-- I'd guess the reason for that is that it's lacking essential structure.
-- Adding a "box" around the exponential solves the problem, but also removes the optimality.
@cheery
cheery / GS2.hs
Created May 20, 2020
Yet another attempt to normalise linear logic (not working)
View GS2.hs
module GS2 where
import Data.STRef
import Control.Monad.ST
import qualified Data.Map as Map
import Data.Map (Map)
-- Terms to normalise
type Arity = (Int, Int, Int)
data Tm
@cheery
cheery / GS2.hs
Created May 14, 2020
Yet another evaluator
View GS2.hs
-- Haven't tested this, may contain trivial bugs.
module GS2 where
import Control.Concurrent
import Control.Concurrent.MVar
-- import qualified Data.Map as Map
-- import Data.Map (Map)
data Ty
= Initial
@cheery
cheery / GS2.hs
Created May 14, 2020
Yet another evaluator
View GS2.hs
-- Haven't tested this, may contain trivial bugs.
module GS2 where
import Control.Concurrent
import Control.Concurrent.MVar
-- import qualified Data.Map as Map
-- import Data.Map (Map)
data Ty
= Initial
@cheery
cheery / graph_reduction.chr
Created Apr 30, 2020
Optimal reduction expressed in CHR
View graph_reduction.chr
/* There may be mistakes here.
This program implements "optimal reduction" in CHR,
it runs in CHR.js playground.
The N in front of each structure is a label.
Rest of the numbers are edges between combinators.
fresh(N) tracks fresh numbers to produce new edges.
*/
eq(X,Y), eq(Y,Z) <=> eq(X,Z)