A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf