Skip to content

Instantly share code, notes, and snippets.

@nvanderw
nvanderw / gist:11004767
Last active Aug 29, 2015
Something catamorphism-like?
View gist:11004767
newtype Fix f = Fix (f (Fix f))
-- Define List as the fixed point of a type operator
data ListR a t = Nil | Cons a t
type List a = Fix (ListR a)
-- The type operator ListR represents "one layer" of the structure
-- of List. We can do something fold-like with it.
-- My question is, is there a name for f? It's like a catamorphism
-- but doesn't recurse into the data.
@nvanderw
nvanderw / PostScript.idr
Last active Aug 29, 2015
Proof-of-concept EDSL for writing PostScript with static stack effects.
View PostScript.idr
module Main
data Literal : Type where
float : Float -> Literal
-- A PostScript program which takes a stack of one size to a stack of
-- another size.
-- (PostScript m n) takes a stack of size m and returns a stack of size n.
data PostScript : Nat -> Nat -> Type where
nop : PostScript n n
@nvanderw
nvanderw / EvenOdd.hs
Created Mar 19, 2014
Proof that numbers go even-odd-even-odd...
View EvenOdd.hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
data Nat = Zero | Succ Nat
data Even :: Nat -> * where
Even_base :: Even Zero
Even_induct :: Even k -> Even (Succ (Succ k))
data Odd :: Nat -> * where
Odd_base :: Odd (Succ Zero)
@nvanderw
nvanderw / Index.hs
Created Mar 19, 2014
Finite sets and safe list indexing
View Index.hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
data Nat = Zero | Succ Nat
-- Bounded naturals
data Fin :: Nat -> * where
FZ :: Fin (Succ n)
FS :: Fin n -> Fin (Succ n)
data Vect (n :: Nat) a where
@nvanderw
nvanderw / Block.elm
Created Feb 22, 2014
Bouncing logo demo
View Block.elm
import Signal
import Window
(block_width, block_height) = (100, 100)
speed = 1.5
dimensions = Window.dimensions
width = lift fst dimensions
height = lift snd dimensions
@nvanderw
nvanderw / Free.ml
Created Feb 14, 2014
Free monads in OCaml, for great referential transparency
View Free.ml
module type Functor = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
end
module type Monad = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val return : 'a -> 'a t
@nvanderw
nvanderw / typeclass.hs
Created Jan 31, 2014
Typeclasses as datatypes
View typeclass.hs
-- Standard Prelude definitions
-- data Ordering = LT | EQ | GT
-- class Eq a => Ord a where
-- compare :: a -> a -> Ordering
isOrdered :: Ord a => [a] -> Bool
isOrdered (x:y:xs) = case compare x y of
GT -> False
_ -> isOrdered (y:xs)
isOrdered _ = True
@nvanderw
nvanderw / Strategy.scala
Last active Jan 3, 2016
Playing abstract strategy games in general
View Strategy.scala
/** Game rules for state space S and players in P */
trait GameRules[S, P] {
/** Score a position relative to a player. That is, a better
position should have a bigger score than a worse one. */
def children(position: S): List[S]
def turn(position: S): P // Whose turn is it on some position?
}
/** Scores positions for a Strategy. R should have a total ordering (see the
* signature of pickMove below) and should be positive if the given player has
View Config.java
interface MaybeVisitor<A, R> {
public R just(A v);
public R nothing();
}
interface Maybe<A> {
public <R> R fold(MaybeVisitor<A, R> visitor);
}
interface PairVisitor<A, B, R> {
@nvanderw
nvanderw / Free.hs
Created Nov 22, 2013
Learning some free monads
View Free.hs
{-# LANGUAGE KindSignatures, GADTs #-}
-- Inspired by the Well-Typed "Monads for Free!" slides, available online
data Free :: (* -> *) -> * -> * where
Return :: a -> Free f a
Wrap :: f (Free f a) -> Free f a
instance Functor f => Functor (Free f) where
fmap f (Return x) = Return (f x)