Skip to content

Instantly share code, notes, and snippets.

View Playground.hs
-- This is a starter contract, based on the Game contract,
-- containing the bare minimum required scaffolding.
-- What you should change to something more suitable for
-- your use case:
-- * The DataScript type
-- * The Redeemer type
-- And add function implementations (and rename them to

Keybase proof

I hereby claim:

  • I am txus on github.
  • I am txus ( on keybase.
  • I have a public key ASAbZcf0hjvViWF-qloQU5qxKk4thtbvBjzXBtKRWAeU9wo

To claim this, I am signing this object:

txus / sessions.clj
Created Feb 20, 2017
Compile-time verification of session-type-like programs in Clojure
View sessions.clj
(require '[clojure.string :as str])
(defn parse [s]
(->> s
(map (fn [line]
(let [[action source destination alternative]
(str/split (str/trim line) #" +")]
{:source source
txus / adts.clj
Created Aug 1, 2016
ADTs with compile-time arity / type checking in Clojure --wip!
View adts.clj
(ns adts
(:require [clojure.string :as str]))
(defn type->kw [ty]
(keyword (str *ns* "/" ty)))
(defn capitalized? [s]
(= (str s) (str/capitalize s)))
(defn adt? [s]
View small_town.cljs
;; person
(def genders #{:male :female})
(defn make-person [age]
{:age age
:gender (rand-nth (vec genders))
:dead false})
txus / incidental_complexity.go
Created May 4, 2016
Getting a random subset of size (N * percentage) of a slice of size N.
View incidental_complexity.go
func RandomSubset(containers []*docker.Container, percentage float64) []*docker.Container {
r := rand.New(rand.NewSource(time.Now().UnixNano()))
length := len(containers)
numberOfElementsWeWant := int64(percentage * float64(length))
randomIndices := r.Perm(length)[0:numberOfElementsWeWant]
var selected []*docker.Container
for _, idx := range randomIndices {
selected = append(selected, containers[idx])
txus /
Last active Mar 15, 2016
Is there a way to have enum branches that introduce their own type parameters?
trait Hey {
fn ha(&self) -> u32;
enum Foo<A> {
Bar<X: Hey>(Box<Fn(X) -> Foo<A>>)
fn test() -> Foo<u32> {
txus /
Last active Jul 30, 2018
Memory as a dependently-typed effect (scroll down for examples!)

Memory as an effect

What if we treated memory as a side-effect?

Idris lets us track lots of things in the type system, in order to get errors at compile-time rather than at runtime. One of the tools that lets us do this in Idris is called Effects, and they're used to keep track of state, to manage file handlers, and lots more.

In barely 40 lines of Idris (which could be less if I had any idea what I'm

txus /
Created Jan 5, 2016
Python is crazy


You'll need dbus running. In a console:


In another console:

View no_queries.cljs
(defui UserView
static om/Ident
(ident [this {:keys [user/id]}]
[:user/by-id id])
static om/IQuery
(query [this]
'[:user/id :user/name :user/authenticated]))
(defui UserProfilesView