Skip to content

Instantly share code, notes, and snippets.

View cdr_police.clj
(ns ture.cdr-police
(:require [overtone.live :refer :all :exclude [stop]]
[leipzig.melody :refer :all]
[leipzig.scale :as scale]
[leipzig.canon :as canon]
[leipzig.live :as live]
[leipzig.live :refer [stop]]
[leipzig.chord :as chord]
[leipzig.temperament :as temperament]))
View FSM.Entropy.idr
module Data.FSM.Entropy
%default total
data Solfege = Do | Re | Mi | Fa | So | La | Ti
entropy : Solfege -> Solfege -> Nat
entropy Do Do = 1
entropy Do Re = 2
entropy Re Do = 2
entropy Re Re = 1
View Entropy.idr
module Entropy
import Data.List
%default total
data Probability : a -> Nat -> Type where
Occurred : (x : a) -> Probability x bits
begin : Probability [] 0
begin = Occurred []
@ctford
ctford / prism.idr
Created Dec 10, 2017
A non-compiling prism implementation where the applicative instance is AWOL.
View prism.idr
module Optic.Prism
import Data.List
%default total
-- Const
data Const a b = Constant a
implementation Functor (Const a) where
map _ (Constant x) = (Constant x)
@ctford
ctford / Chain.idr
Created Nov 4, 2017
Fuse a chain of functions
View Chain.idr
module Data.Chain
%default total
data Chain : Type -> Type -> Type
where
Link : (a -> b) -> Chain a b
Section : (a -> b) -> Chain b c -> Chain a c
fuse : Chain a b -> a -> b
fuse (Link f) x = f x
@ctford
ctford / channel.idr
Last active Oct 29, 2017
A simple example of dual client/server session types.
View channel.idr
module Data.FSM.Channel
import Data.List
%default total
data Protocol : Type
where
Out : a -> Protocol -> Protocol
In : a -> Protocol -> Protocol
Accept : Protocol -> Protocol -> Protocol
Select : Protocol -> Protocol -> Protocol
@ctford
ctford / channel.idr
Created Oct 22, 2017
The totality checker thinks `dual` the last case of makes it partial - even though I would have thought the pattern matching shrinks the argument.
View channel.idr
%default total
data Channel : (result :Type ) -> Type
where
Send : a -> Channel a
Receive : a -> Channel a
Finished : Channel ()
(>>=) : Channel a -> ((x:a) -> Channel b) -> Channel b
dual : Channel a -> Channel a
@ctford
ctford / song.clj
Created May 27, 2017
Whilst you were
View song.clj
(ns whilst.song
(:require [overtone.live :refer :all]
[leipzig.melody :refer :all]
[leipzig.scale :as scale]
[leipzig.live :as live]
[leipzig.chord :as chord]
[leipzig.temperament :as temperament]))
; Instruments
(definst bass [freq 110 dur 1 volume 1.0]
@ctford
ctford / when.idr
Created Feb 17, 2017
A safe test that returns different types in the if and the else branches.
View when.idr
when : (test : Bool) -> a -> b -> if test then a else b
when True x _ = x
when False _ y = y
@ctford
ctford / locate.idr
Created Feb 12, 2017
A function that uses a membership proof to safely locate a tuple in a list.
View locate.idr
locate : Eq a => (key : a) -> (entries : List (a, b)) -> {auto membership : Elem key (map Prelude.Basics.fst entries)} -> b
locate {membership} _ [] = absurd membership
locate {membership = Here} key ((key, value) :: _) = value
locate {membership = (There later)} key (_ :: entries) = locate key entries {membership = later}