[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The following SML program
exception C;
structure M :> sig exception A end =
struct
exception A = C
end;
(raise M.A) handle C => 42
returns the value 42 (according to SML/NJ and, I believe, the 1997
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Phil,
I learned about this from Martin Escardo, and he told me the observation
about monoidal closure is in Lawvere's paper "Metric Spaces, Generalized
Logic, and Closed Categories".
One further observation I have
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, Sam.
I would take issue with your characterization of this example as
"breaking abstraction". By way of analogy, when you opaquely seal a
module with a signature containing a field
val v : T,
it does not mean
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks Derek.
My subject line is deliberately provocative. Given that exceptions in ML are
values that inhabit a single type, the behaviour does make sense, and is rather
unsurprising if we rewrite M as:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I am not sure whether the following is the correct definition of a monus,
but following Neel (as well as the analogy with natural numbers) one could
look at monus in a monoid as right adjoint to monoid multiplication. In
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
While I cannot comment on how often this occurs in practice, I'd like to
point out that this ability to hide equalities between exceptions has
delicate implications for the compilation of pattern-matching (in
