Skip to content

Instantly share code, notes, and snippets.

View conal's full-sized avatar

Conal Elliott conal

View GitHub Profile
@conal
conal / quiver-macros.tex
Last active July 28, 2021 23:14
Some q.uiver.app macros
\newcommand\AF[1]{{\textsf #1}}
@conal
conal / NatStream.hs
Last active August 29, 2015 14:18
Isomorphism between streams and function-of-Nat
{-# OPTIONS_GHC -Wall #-}
module NatStream where
data Nat = Zero | Succ Nat
data Stream a = a :< Stream a
-- Stream is the trie induced by Nat.
-- Here's the isomorphism, explicitly:
@conal
conal / backus-denotational-design.md
Last active August 27, 2022 16:54
John Backus on denotation for design

From section 9 of John Backus's 1977 Turing Award lecture Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs:

Denotational semantics and its foundations provide an extremely helpful mathematical understanding of the domain and function spaces implicit in programs. When applied to an applicative language (...), its foundations provide powerful tools for describing the language and for proving properties of programs. When applied to a von Neumann language, on the other hand, it provides a precise semantic description and is helpful in identifying trouble spots in the language. But the complexity of the language is mirrored in the complexity of the description, which is a bewildering collection of productions, domains, functions, and equations that is only slightly more helpful in proving facts about programs than the reference manual of the language, since it is less ambiguous.

...

Thus