Skip to content

Instantly share code, notes, and snippets.

View voila's full-sized avatar

voila

24 followers · 5 following
  • Dunedin, NZ
View GitHub Profile
@lmarburger
lmarburger / expr.idr
Last active August 29, 2015 14:02
Extending Idris tutorial 4.4.1 to include a Let operation
data Expr = Var String
| Val Int
| Add Expr Expr
| Let (List (String, Int)) Expr
data Eval : Type -> Type where
MkEval : (List (String, Int) -> Maybe a) -> Eval a
fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
@jozefg
jozefg / queue.idr
Last active August 29, 2015 14:14
Queue in Idris
module queue
import Data.Vect
-- Here's the port of the Liquid Haskell blog post on amortized
-- queues. The tricksy bit is that the "amortized" bit depends on
-- laziness. This means that while in the REPL (where Idris is lazy)
-- this is reasonably efficient. It compiles absolutely horribly
-- though because each time push or pop something we rotate the whole
-- damned thing.
@johnynek
johnynek / stref.scala
Last active November 10, 2015 19:47
mutable variables via a state thread in scala. This is just meant as an illustration of how ST in haskell works, and more generally, how you can implement mutation with immutable APIs.
object STRef {
/**
* Here is a container where we have a single "state thread" = ST.
* When we run this thread of type ST[T] we get a result of type T.
*/
sealed abstract class ST[+T] {
def map[R](fn: T => R): ST[R] = flatMap(t => Const(fn(t)))
def flatMap[R](fn: T => ST[R]): ST[R] = FlatMapped(this, fn)
}
@npwolf
npwolf / led_controller.erl
Created February 27, 2013 16:34
%%% led_controller is a module to toggle LEDs wired to gpio pins on the raspberry pi
-module(led_controller).
-behavior(gen_server).
-export([start_link/1]).
% standard gen_server
-export([init/1, handle_call/3, handle_cast/2, handle_info/2, terminate/2, code_change/3]).
% Public Interface
-export([on/1, off/1, blink/2]).
% Don't call these directly
-export([blink_cast/2]).
@raichoo
raichoo / gist:5700522
Last active December 18, 2015 00:59
JavaScript Lib
module Main
{-
Compile with:
idris --package javascript --target javascript test.idr -o test.js
<html>
<head>
@fitzgen
fitzgen / go.js
Created August 30, 2013 20:07
http://swannodette.github.io/2013/08/24/es6-generators-and-csp/ ported to SpiderMonkey (at least until ES6 generators are fully supported, which should be within the next month or so)
function go_(machine, step) {
while(!step.done) {
try {
var arr = step(),
state = arr[0],
value = arr[1];
switch (state) {
case "park":
setImmediate(function() { go_(machine, step); });
@sdiehl
sdiehl / Homomorphisms.hs
Last active December 22, 2015 07:59
{-# Language GADTs #-}
module Homomorphisms where
import Control.Monad
import Control.Applicative
import Data.Monoid hiding (Endo)
import qualified Control.Category as C
@timjb
timjb / AboutMe.mustache
Created December 1, 2013 15:27
Mustache templating in Idris
Hello, my name ist {{name}} and I am {{age}} years old.
@NicolasT
NicolasT / Connection.hs
Last active December 30, 2015 09:09
Compile-time enforced resource exhaustion in OCaml using an indexed state monad.
{-# LANGUAGE RebindableSyntax,
KindSignatures,
DataKinds,
GADTs,
GeneralizedNewtypeDeriving,
StandaloneDeriving,
FlexibleInstances,
Rank2Types #-}
module Connection (
@jlongster
jlongster / gruntfile.js
Created December 19, 2013 20:38
gruntfile
var fs = require('fs');
var path = require('path');
var sweet = require('sweet.js');
module.exports = function(grunt) {
grunt.initConfig({
sweetjs: {
options: {
modules: ['es6-macros'],
sourceMap: true,