If you are a professional mathematician and you are asked whether 2 + 2 = 4, the only answer you should give is “Yes, obviously.”
October 14, 2020 / retroactive, note-to-self
If you are a professional mathematician and you are asked whether 2 + 2 = 4, the only answer you should give is “Yes, obviously.”
July 12, 2019 / note-to-self, retroactive
Here are most of the cocktails in the IBA cocktail list ordered such that as you go down, at most one new cocktail ingredient each time is needed. (This doesn’t include other ingredients such as fruit juice.)
July 8, 2019 / note-to-self, should-have-known
These answers can be found just by Googling, but it’s nice to have a record of things I’ve wondered about.
Why do jetskis spit that jet of water vertically?
This is apparently just for visibility, there is a little pipe attached to the outlet that faces upward. A lot of people plug it so they don’t spray passengers or nearby people.
Why is orange juice usually from concentrate?
Easier to package and transport.
Why do American school buses look more or less identical?
Road rules are different around school busses; in particular, the stop sign that pops out from the side stops traffic in both directions. For this reason it is important that they are easily identifiable. The yellow is said to be more eye-catching in peripheral vision than other colours.
What are blackboards made of?
These days, porcelain enamel on a steel base. They are often green rather than black, the thinking being that the green paint reduces glare compared to black.
What are the square, Asian-looking stamps sometimes present on the title page of old books?
Those are ‘seals’, signatures in stamp form. The books I’m thinking of must have once been owned by someone who had their own seal.
What is the connection between barbers and red/white striped poles?
One of the services that medieval “barber-surgeons” would perform was blood-letting. The pole represents the staff that patients would grip to make their veins pop, and the red and white colouring represents the bloody bandages that would be hung outside the shop to dry.
Why do signs give the maximum fine for disobeying them? Wouldn’t a minimum be more persuasive?
Typically people are given the maximum penalty, so the value shown is the fine that any would-be lawbreakers should expect. However, it is better for judges to be able to use discretion on exactly what fine is imposed in specific situations.
Why do so many recipe websites have long boring stories before the recipes?
Some people like to waffle, but a big reason is ad revenue and SEO. Long and detailed text causes visitors to spend more time on your site, and gives more opportunities to include relevant search keywords.
Were people just killed by acute appendicitis before modern surgery?
Yes.
Why are bay leaves typically not ground up like other herbs?
The flavour of bay leaves is overpoweringly strong when ground up, even in very small amounts.
What is the cause of the ‘fingernails on a blackboard’ response?
The cause is currently unknown, but there are some theories.
One hypothesis is that the sound is similar to the alarm call of some monkeys and the instinct to cringe dates back to early human evolution. Another is that the sound is “the ultimate dissonance”, and is unpleasant for the same reason that dissonant music is unpleasant.
Interestingly, tests showed that it is the middle frequencies (2000Hz to 4000Hz) that cause the instinctive reaction, not the high frequencies as one might expect.
January 10, 2019 / note-to-self, cringe, rolling
Some words and phrases encountered while reading. Of course, it’s embarrassing to air this list in public. How could I not know that word?
February 10, 2018 / note-to-self, code, retroactive
Hamana describes a neat way of encoding general graphs as a GADT in
Initial Algebra Semantics for Cyclic Sharing Tree
Structures, a nice trick that I
hadn’t seen before. The idea is that the Graph
data type will have a
Ptr
constructor that allows us to add an edge reference other parts
of the structure. The Graph
type will be indexed by a ‘context’ that
specifies what Ptr
s are valid.
Elements of Graph
won’t correspond to general graphs exactly. We are
actually describing graphs that are “rooted, connected, directed and
edge-ordered with each node having out-degree 2”. It is possible to
choose different roots and orderings for the same graph, and these
choices will lead to different representations as elements of
Graph
. The problem of determining whether two elements of Graph
have the same underlying actual graph seems like it would be difficult
in general.
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module Graphs where
First, let us define a type describing the possible shapes of our data
structure. We will be using this at the type-level via DataKinds. Our
Graph
s all have underlying binary trees.
data TreeShape where
LeafShape :: TreeShape
BinShape :: TreeShape -> TreeShape -> TreeShape
There are also special leaves that are Ptr
s to other locations.
PtrShape :: TreeShape
And finally, we will need a way of blocking off a section of a graph
so that a Ptr
can’t refer to it.
VoidShape :: TreeShape
This won’t occur as the shape of an actual graph.
The next piece is an indexed type that, given a TreeShape
, picks
out the location of a node in that shape. These will be what we use to
specify where in a tree a Ptr
is pointing.
data TreePosition (shape :: TreeShape) where
LeafPos :: TreePosition LeafShape
BinPos :: TreePosition (BinShape s t)
LeftPos :: TreePosition s -> TreePosition (BinShape s s')
RightPos :: TreePosition s' -> TreePosition (BinShape s s')
There is, of course, no constructor for TreePosition VoidShape
. We
also don’t allow TreePosition PtrShape
, which means that Ptr
s
will be required to point to genuine nodes in the tree, and not other
Ptr
s. This avoids there being multiple ways of specifying the same
tree via chains of pointers, rather than having each Ptr
target the
eventual node at the end of the chain.
We’ll need to be able to index type-level lists, so let’s get that out of the way:
data Elem :: k -> [k] -> * where
Here :: Elem s (s : c)
There :: Elem s c -> Elem s (t : c)
Now for the actual graph type. The type is indexed both by the shape
of the underlying tree, and a context
, a list of TreeShape
s. As we
build a tree, this list is collecting the shapes of all the subtrees
used as a left branch of an earlier binary node.
Consider the following tree:
a
/ \
/ \
a b
/ \ / \
a a b *
\
b
If we are currently defining the subtree to be placed at *
, then the
context
will consist of the two shapes
a
b / \
/ \ / \
[ b 0 , a 0 ]
\ / \
b a a
In the subtree to be placed at *
, we may have pointers to a
s or b
s,
but not the 0
s.
data Graph (context :: [TreeShape]) (shape :: TreeShape) where
Leaf :: Graph c LeafShape
Leaves are easy, we can have a leaf in any context.
Ptr :: Elem s context -> TreePosition s -> Graph context PtrShape
For the pointers, we pick a shape from the context and then a position in that shape.
Bin :: Graph (BinShape VoidShape VoidShape : c) s
-> Graph (BinShape s VoidShape : c) t
-> Graph c (BinShape s t)
The interesting case is a binary node. In the left and right branches,
we push new trees onto the context c. When defining the left branch,
we only have access to one additional node over what is already in
c
: the binary node we are currently defining. In the right branch,
we have access to the entire left branch: note that the shape s
of
the left branch is what is pushed onto the context. This is why this
type has to be indexed over the shape of the resulting graph, not just
the context.
And that’s it! We can add labels to the nodes in the graph if we like,
by adding a parameter to the Leaf
and Bin
constructors.
Graphs of shape s
then correspond to elements of Graph '[] s
. If
we don’t care about having the shape as part of the type, we can
existentially quantify it.
data AnyGraph = forall s. AnyGraph (Graph '[] s)
Here are some simple graphs:
graph1 :: AnyGraph
= AnyGraph $ Bin (Bin Leaf Leaf) (Bin (Ptr (There $ Here) (LeftPos $ LeftPos $ LeafPos)) Leaf) graph1
Corresponding to
*
/ \
/ \
* *
/ \ / \
* * / *
\ /
---
We can modify what kinds of graphs are representable by changing the
way the context
is extended. Note that we can currently have cycles
in the graph:
graph2 :: AnyGraph
= AnyGraph $ Bin Leaf (Ptr Here BinPos) graph2
corresponds to
---
/ \
* /
/ \ /
* --
It’s not hard to change this though:
data DAG (context :: [TreeShape]) (shape :: TreeShape) where
DAGLeaf :: a -> DAG c LeafShape
DAGPtr :: Elem s context -> TreePosition s -> DAG context PtrShape
DAGBin :: DAG c s -> DAG (s : c) t -> DAG c (BinShape s t)
The only difference is in the DAGBin
constructor. Here, when
constructing the left branch, we are no longer permitted to reference
the current binary node. The same is true when constructing the right
branch, but we still give it access to the left branch. The result is
that every Ptr
points to something to the left, other than a direct
ancestor of the current node. That is enough to rule out any cycles.
We have no need for VoidShape
here, which is nice.