I was recently working on some Haskell code (for research, with Jack Hughes) and happened to be using a monoid (via the Monoid type class) and I was rushing. I accidentally wrote x `mempty` y instead of x `mappend` y. The code with mempty type checked and compiled, but I quickly noticed some tests giving unexpected results. After a pause, I checked the recent diff and noticed this mistake, but I had to think for a moment about why this mistake was not leading to a type error. I thought this was an interesting little example of how type class instance resolution can sometimes trip you up in Haskell, and how to uncover what is going on. This also points to a need for GHC to explain its instance resolution, something others have thought about; I will briefly mention some links at the end.
The nub of the problem
In isolation, my mistake was essentially this:
whoops :: Monoid d => d -> d -> d
whoops x y = mempty x y -- Bug here. Should be "mappend x y"
So, given two parameters of type d for which there is a monoid structure on d, we use both parameters as arguments to mempty.
Recall the Monoid type class is essentially:
class Monoid d where mempty :: d mappend :: d -> d -> d
(note that Monoid also has a derived operation mconcat and is now decomposed into Semigroup and Monoid but I elide that detail here, see https://hackage.haskell.org/package/base-4.14.0.0/docs/Prelude.html#t:Monoid).
We might naively think that whoops would therefore not type check since we do not know that d is a function type. However, whoops is well-typed and evaluating
whoops [1,2,3] [4,5,6] returns []. If the code had been as I intended, (using mappend here instead of mempty) then we would expect [1,2,3,4,5,6] according to the usual monoid on lists.
The reason this is not a type error is because of GHC’s instance resolution and the following provided instance of `Monoid`:
instance Monoid b => Monoid (a -> b) where mempty = \_ -> mempty mappend f g = \x -> f x `mappend` g x
That is, functions are monoids if their domain is a monoid with mempty as the constant function returning the mempty element of b and mappend as the pointwise lifting of a monoid to a function space.
In this case, we can dig into what is happening by compiling1 with --ddump-ds-preopt and looking at GHC’s desugared output before optimisation, where all the type class instances have been resolved. I’ve cleaned up the output a little (mostly renaming):
whoops :: forall d. Monoid d => d -> d -> d
whoops = \ (@ d) ($dMonoid :: Monoid d) ->
let
$dMonoid_f :: Monoid (d -> d)
$dMonoid_f = GHC.Base.$fMonoid-> @ d @ d $dMonoid }
$dMonoid_ff :: Monoid (d -> d -> d)
$dMonoid_ff = GHC.Base.$fMonoid-> @ (d -> d) @ d $dMonoid_f }
in
\ (x :: d) (y :: d) -> mempty @ (d -> d -> d) $dMonoid_ff x y
The second line shows whoops has a type parameter (written @ d) and the incoming dictionary $dMonoid representing the Monoid d type class instance (type classes are implemented as data types called dictionaries, and I use the names $dMonoidX for these here).
Via the explicit type application (of the form @ t for a type term t) we can see in the last line that mempty is being resolved at the type d -> d -> d with the monoid instance Monoid (d -> d -> d) given here by the $dMonoid_ff construction just above. This is in turn derived from the Monoid (d -> d) given by the dictionary construction $dMonoid_f just above that. Thus we have gone twice through the lifting of a monoid to a function space, and so our use of mempty here is:
mempty @ (d -> d -> d) $dMonoid_ff = \_ -> (\_ -> mempty @ $dMonoid)
thus
mempty @ (d -> d -> d) $dMonoid_ff x y = mempty @ d $dMonoid
That’s why the program type checks and we see the mempty element of the original intended monoid on d when applying whoops to some arguments and evaluating.
Epilogue
I luckily spotted my mistake quite quickly, but this kind of bug can be a confounding experience for beginners. There has been some discussion about extending GHCi with a feature allowing users to ask GHC to explain its instance resolution. Michael Sloan has a nice write up discussing the idea and there is a GHC ticket proposing by Icelandjack something similar which seems like it would work well in this context where you want to ask what the instance resolution was for a particular expression. There are many much more confusing situations possible that get hidden by the implicit nature of instance resolution, so I think this would be a very useful feature, for beginner and expert Haskell programmers alike. And it certainly would have explained this particular error quickly to me without me having to scribble on paper and then check --ddump-ds-preopt to confirm my suspicion.
Additional: I should also point out that this kind of situation could be avoided if there were ways to scope, import, and even name type class instances. The monoid instance Monoid b => Monoid (a -> b) is very useful, but having it in scope by default as part of base was really the main issue here.
1 To compile, put this in a file with a main stub, e.g.
main :: IO () main = return ()
. For example, take 
and 
to be notions of program equivalence (equivalent inputs produce equivalent outputs). Another relation might be in information-flow security where relations 
mean “these two programs are low-level equivalent” (low-security).![S(Y_!, Y_@) = Pr[Y_1] \leq e^\epsilon Pr[Y_2]](https://s0.wp.com/latex.php?latex=S%28Y_%21%2C+Y_%40%29+%3D+Pr%5BY_1%5D+%5Cleq+e%5E%5Cepsilon+Pr%5BY_2%5D&bg=ffffff&fg=000000&s=0&c=20201002)
.
(giving an upper bound computed in terms of the inputs and underlying relations). This is useful for guaranteeing compile optimisations (not worse, or definitely better), ruling out side-channel attacks (i.e., the ![\textsf{cost}(e[v_1/x]) - \textsf{cost}(e[v_2/x]) = 0](https://s0.wp.com/latex.php?latex=%5Ctextsf%7Bcost%7D%28e%5Bv_1%2Fx%5D%29+-+%5Ctextsf%7Bcost%7D%28e%5Bv_2%2Fx%5D%29+%3D+0&bg=ffffff&fg=000000&s=0&c=20201002)
, such that different inputs do not yield different costs thus information about the inputs is not leaked).
in length).
. Talk about relational properties of the input and relational properties of the output. Usually, if we interpret to relations then we want to prove soundness as: ![(\bar{v_1}, \bar{v_2}) \in [\Gamma] \Rightarrow ([t_1[\bar{v_1}/\Gamma]], t_2[\bar{v_2}/Gamma]]) \in [\tau]](https://s0.wp.com/latex.php?latex=%28%5Cbar%7Bv_1%7D%2C+%5Cbar%7Bv_2%7D%29+%5Cin+%5B%5CGamma%5D+%5CRightarrow+%28%5Bt_1%5B%5Cbar%7Bv_1%7D%2F%5CGamma%5D%5D%2C+t_2%5B%5Cbar%7Bv_2%7D%2FGamma%5D%5D%29+%5Cin+%5B%5Ctau%5D&bg=ffffff&fg=000000&s=0&c=20201002)
.\
where 
is the upper bound and 
is the lower bound execution cost, which are thought of as a unary effect. A relational judgement 
where 
is the upper bound on the relative cost of the two programs. The types have an annotation function type (like in normal effect systems) 
and data types for integers and lists have indices to express dependencies.
.
this can be refined (with the type ![n : \textsf{int}[5]](https://s0.wp.com/latex.php?latex=n+%3A+%5Ctextsf%7Bint%7D%5B5%5D&bg=ffffff&fg=000000&s=0&c=20201002)
in the indices, which will change the bound to $\vdash^{k+1}_{k+1}$.
.
.
.
captures lists which differ in less than 
positions. This interacts with the 
type in order to capture the notion of differing numbers of elements in the list.
and 
meaning 
has a relatively smaller cost. Plugging this into the higher-order function and doing the type derivation again gives a looser bound.
which contains term variable assertions 
and relational assertion 
. In the type system, some rules are synchronous (building up the related two terms with the same syntactic construct) or asynchronous (building up one of the terms).
is a monadic meta language with a specific cost effect (with 
introducing a cost. Intuition: if a term 
is closed and $m \Downarrow_n v$ then $m \cong \textsf{cstep}_n(v)$.We can define formulae in HOL which all us to reason about these explicit cost terms and their quantities: we can define what we need in the logic.
. Using the system , we can prove this property, using a suitable invariant/predicate over the input and output list(s).
.
(I forgot what the constant c was). This work introduces references and arrays to enable analysis of programs where resource consumption depends on the data stored in mutable structures (references and arrays).
that is it can contribute 
units of potential where 
across the two variables. Benjamin walked us through a nice example with appending to a list.
is the principle type of 
if 
and for all types 
such that 
there exists a substitution 
.
is inhabited by the K combinator 
but is not principally inhabited (
. Define relations on paths, 
as the minimal equivalence relation for a beta-normal term 
which defines an equivalence relation on paths of paths with common subpaths (capture constraints on subformulae on types).
(note the two occurrences of 
) where intersection is associative, commutative and (possibly) idempotent. In 1994, Gardner introduces a system which is not idempotent, where types are now multisets (rather than sets in the earlier formulations). This has the flavour of linear logic resources (
)
implies 
which can be provided by relational parametricity, see Reynolds “related things map to related things”, applies identity extension lemma).
is however 
. Suppose $B = U$ then we can leak details of the implementation (rerepresentation type is returned as data) 
(has this type). This violates the identity extension lemma used in the above proof for System F.
ill typed. The proof of parametricity for 
(cf Bernardy, Coquand, and Moulin 2015, on bridge/path-based proofs) which gives a basis for proving the core idea of “related things map to related things” where 
is connected with the type 
(in the above type) and 
is connected to the type 
via a switching term 
(see paper for the proof) (I think this is analogous to setting up a relation between 
, you can define 
.
but also 
. Intuition: sizes are irrelevant in terms, but relevant in types only.
, where sizes uses as indexes can be marked as irrelevant in the context. Here is one of the rules for type formation when abstracting over an irrelevantly typed argument:
for necessity (true without any hypotheses) 
(if something A is possible true then possibility can propagate to the context– doesn’t change the “possibleness”). Various intuitionistic substructural and modal logics/type systems: linear/affine, relevant, ordered, bunched (separation logic), coeffects, etc. Cohesive HoTT: take dependent type theory and add modalities (int, sharp, flat). S-Cohesion (Finster, Licata, Morehouse, Riley: a comonad and monad that themselves are adjoint, ends up with two kind of products which the modality maps between). Motivation: what are the common patterns in substructural and modal logics? How do we construct these things more systematically from a a small basic calculus.
which is modelled by 
. In the sequent calculus style, use the notion of context to form the type. Linear logic ! is similar (but with no weakening). The rules for 
follow the same kind of pattern: e.g., 
where the context “decays” into the logical operator (rather than being literally equivalent): the types inherent the properties of the context (cf. also exchange).
where 
is this context descriptor. Context descriptors are built on “modes”. e.g., 
the meaning of this sequent depends on the equations/inequations on the context descriptor:, e.g.,if you have associativity of 
then you get a relevant logic, etc. Bunched implication will have two kinds of nodes in the context descriptor. For a modality, unary function symbols, e.g. 
means that the left part of the context is wrapped by a modality.
where we have weakend in the sequent calculus but the context descriptor is unchanged (i.e., we can’t use 
to prove 
. All of the left rules become instances of one rule on F: ![\dfrac{\Gamma, \Delta \vdash_{\beta[\alpha / x]} B}{\Gamma, x : F_\alpha(\Delta) \vdash B}](https://s0.wp.com/latex.php?latex=%5Cdfrac%7B%5CGamma%2C+%5CDelta+%5Cvdash_%7B%5Cbeta%5B%5Calpha+%2F+x%5D%7D+B%7D%7B%5CGamma%2C+x+%3A+F_%5Calpha%28%5CDelta%29+%5Cvdash+B%7D&bg=ffffff&fg=000000&s=0&c=20201002)
which gives you all your left-rules (a related dual rule gives the right sequent rules).
and 
where the first parameter is contravariant and second is covariant may have dinatural transformations between them. (Dinaturality is weaker than naturality). Yields a family of maps 
which separate the contravariant and covariant actions in the coherence condition (see 
and proofs/terms by dinautral transformations. Due to Girard, Scedrov, Scott 1992 there is the theorem that: if 
then 
-normal and (syntactically) dinatural then 
– this is a dinatural transformation and its dinaturality hexagon is representable by lambda terms.
then $n \leq h$, there are various others; see paper).
) of types in a universe 
every identification 
induces an (Id)-isomorphism 
. U is univalent “if all Id-isomorphisms 
” (want this expressed in type theory) (this is a simpler restating of Voevodsky’s original definition due to Licata, Shulman, et al.). This paper: towards answering, are there models for usual type theory which contain such univalent universes?
implies 
. Univalence is telling you that the notion of identification is richer subsuming ETT where there is an identification between two types then they are already equal, which is much smaller/thinner.
are paths from point 
in a space 
is a “constant path” (transporting along such a path does nothing to the element).
for these identifications, but we need to restrict to families of type 
carrying structure to guarantee substitution operations (in this DTT context). “Holes” is diagrams are filled using path reversals and path composition. Solution is “Moore” paths.
in 
and an extent function 
satisfying 
and 
. These paths have a reversal operator by truncated subtraction 
. (note this is idempotent on constant paths as required, allowing holes in square paths to be filled (I had to omit the details, too many diagrams)). But topological spaces don’t give us a model of MLTT, so they replace it by an arbitrary topos (modelling extensional type theory) and instead of 
for path length/shape use any totally ordered commutative ring. All the definition/properties of Moore paths are the expressed in the internal language of the topos. This successfully gives you a category with families (see Dybjer) modelling intensional Martin-Lof type theory (with Pi). This also satisfies dependent functional extensionality thus its probably a good model as univalence should imply extensionality. But haven’t yet got a proof that this does contain a univalence universe (todo).
[Ahmed, Findler, Siek, Wadler POPL’11] (fixed a few problems) and proves parametricity for it.![\lambda x . x + 1 : \ast \Rightarrow^p \forall X . X \rightarrow X) [int] 4](https://s0.wp.com/latex.php?latex=%5Clambda+x+.+x+%2B+1+%3A+%5Cast+%5CRightarrow%5Ep+%5Cforall+X+.+X+%5Crightarrow+X%29+%5Bint%5D+4&bg=ffffff&fg=000000&s=0&c=20201002)
returns 5 but we want to raise a “blame” for the coercion 
here (coercing a monomorphic to polymorphic type is bad!).
(that is, casts to the dynamic type and back again cancel out).
(
this has a type that makes it look like a constant function 
. When executing this we want to raise blame rather than actually produce a value (e.g. for ![add 3 [\textsf{int}] 2](https://s0.wp.com/latex.php?latex=add+3+%5B%5Ctextsf%7Bint%7D%5D+2&bg=ffffff&fg=000000&s=0&c=20201002)
). Solution: use runtime type generation rather than substitution for type variables.
provides a dictionary mapping type variables to types.![\Sigma \rhd (\Lambda X . v) [B] \mapsto \Sigma, \alpha := B \rhd v[\alpha/X]](https://s0.wp.com/latex.php?latex=%5CSigma+%5Crhd+%28%5CLambda+X+.+v%29+%5BB%5D+%5Cmapsto+%5CSigma%2C+%5Calpha+%3A%3D+B+%5Crhd+v%5B%5Calpha%2FX%5D&bg=ffffff&fg=000000&s=0&c=20201002)
i.e., instead of substituting the ![\Sigma \rhd (\Lambda X . v) [B] \mapsto \Sigma, \alpha := B \rhd v[\alpha/X] : A[\alpha/X] \Rightarrow^{+\alpha} A[B/X]](https://s0.wp.com/latex.php?latex=%5CSigma+%5Crhd+%28%5CLambda+X+.+v%29+%5BB%5D+%5Cmapsto+%5CSigma%2C+%5Calpha+%3A%3D+B+%5Crhd+v%5B%5Calpha%2FX%5D+%3A+A%5B%5Calpha%2FX%5D+%5CRightarrow%5E%7B%2B%5Calpha%7D+A%5BB%2FX%5D&bg=ffffff&fg=000000&s=0&c=20201002)
where 
(
are tuples of the type-name stores, and relations about when concealed values should be related. See paper: also shows soundness of the logical relations wrt. contextual equivalence. There was some cool stuff with “concealing” that I missed really.
where 
defines type consistency. Idea: extend this to include notions of consistency between polymorphic and dynamic types. An initial attempt breaks conservativity since there are ill-typed System F terms which are well-typed in System Fg then.
– 
so that it can not be used inside of 
(term level) and 
(type level).
. But inference is highly non-trivial.
and 
(here the natural number has a size too).
. Then we need to find a concrete interpretation of 
.
.
This has been used mainly to make termination arguments.
induces a multiset path order 
, (
if 
is 
, or 
some 
(recursive function to create a splay tree). A type system for this was shown, with cost annotation judgment (no time to copy down any details).
(Hillerstrom, Lindley 2016) – lambda calculus with effect handlers (separate syntactic category but contains lambda terms), row polymorphism, and monadic metalanguage style constructs for effectful let binding and ‘return’. The CPS translation is a homomorphism on all the lambda calculus syntax, but continuation passing on the effectful fragment (effectful let and return). One part of the interpretation for the effectful operation term: ![[[\textbf{do} \, l \, V]] = \lambda k . \lambda h . \; h (l \; \langle[[V]], \lambda x . k \; x \; h\rangle)](https://s0.wp.com/latex.php?latex=%5B%5B%5Ctextbf%7Bdo%7D+%5C%2C+l+%5C%2C+V%5D%5D+%3D+%5Clambda+k+.+%5Clambda+h+.+%5C%3B+h+%28l+%5C%3B+%5Clangle%5B%5BV%5D%5D%2C+%5Clambda+x+.+k+%5C%3B+x+%5C%3B+h%5Crangle%29&bg=ffffff&fg=000000&s=0&c=20201002)
(
These can be used to express monotonicity properties, are syntax directed, and exploit structural similarities of code. However, say we want to prove the naturality of 
where 
is a binary predicate on properties of the two terms and ![\dfrac{\Gamma, x_1 : \sigma_1, x_2 : \sigma_2 \mid \Psi, \phi' \vdash t_1 : \tau_1 \sim t_2 : \tau_2 \mid \phi} {\Gamma \mid \Psi \vdash \lambda x_1 : t_1 : \sigma_1 \rightarrow \tau_1 \sim \lambda x_2 . t_2 : \sigma_2 \rightarrow \tau_2 \mid \forall x_1 . \phi' \Rightarrow \phi[r_1 x_1 / r_1, \, r_2 x_2 / r_2]}](https://s0.wp.com/latex.php?latex=%5Cdfrac%7B%5CGamma%2C+x_1+%3A+%5Csigma_1%2C+x_2+%3A+%5Csigma_2+%5Cmid+%5CPsi%2C+%5Cphi%27+%5Cvdash+t_1+%3A+%5Ctau_1+%5Csim+t_2+%3A+%5Ctau_2+%5Cmid+%5Cphi%7D+%7B%5CGamma+%5Cmid+%5CPsi+%5Cvdash+%5Clambda+x_1+%3A+t_1+%3A+%5Csigma_1+%5Crightarrow+%5Ctau_1+%5Csim+%5Clambda+x_2+.+t_2+%3A+%5Csigma_2+%5Crightarrow+%5Ctau_2+%C2%A0%5Cmid+%5Cforall+x_1+.+%5Cphi%27+%5CRightarrow+%5Cphi%5Br_1+x_1+%2F+r_1%2C+%5C%2C+r_2+x_2+%2F+r_2%5D%7D&bg=ffffff&fg=000000&s=0&c=20201002)
.
? It depends on call-by-value, call-by-name, call-by-need, or full beta then you get different answers. The call-by-value, call-by-name, and call-by-need strategies are called weak because they do not reduce underneath lambda abstraction. As a consequence, they do not compute normal forms on their own.![t[v[u/y]/x] \rightarrow t[u/y][v/x]](https://s0.wp.com/latex.php?latex=t%5Bv%5Bu%2Fy%5D%2Fx%5D+%5Crightarrow+t%5Bu%2Fy%5D%5Bv%2Fx%5D&bg=ffffff&fg=000000&s=0&c=20201002)
).
only when the number of reference to 
is less than or equal to 1 (so things don’t explode).
(agent ‘a’ believes A)![[\alpha] A](https://s0.wp.com/latex.php?latex=%5B%5Calpha%5D+A&bg=ffffff&fg=000000&s=0&c=20201002)
(A holds true after action 
– multiples of 3 in binary.
![[-] : 2^{\textsf{Pom}_{\Sigma}}](https://s0.wp.com/latex.php?latex=%5B-%5D+%3A+2%5E%7B%5Ctextsf%7BPom%7D_%7B%5CSigma%7D%7D&bg=ffffff&fg=000000&s=0&c=20201002)
.
then terminates.
not 
. (I wasn’t sure if this was an open question or whether there was a solution in this paper).
, e.g., scan [1,2,3,4] = [1,3,6,10]
is a 4-vector.
. This work shows the formal relation (that indeed these two systems are equivalent). A proof is partially given in Geuvers ’93, but a full Coq formalisation was given by Kaiser, Tebbi and Smolka at POPL 2017. In this work, the proof is replayed across three tools to provide a useful comparison of the three systems: Coq, Abella and Beluga.
in PTS can correspond to 
and 
. Have to also keep track of context assumptions. One (of many) “topics of interest” in this comparison is how to manage contexts (which is interesting to me as I am quite interested in CMTT in Beluga).
that gives it meaning ![[\Gamma \vdash K]](https://s0.wp.com/latex.php?latex=%5B%5CGamma+%5Cvdash+K%5D&bg=ffffff&fg=000000&s=0&c=20201002)
. There is no concept of free variable., e.g., in Coq 
is provable but in Belluga 
is ![\textsf{scale} \; (c : \mathbb{R}) \; (n : [\textsf{abs} \; c] \mathbb{R}) : \mathbb{R}](https://s0.wp.com/latex.php?latex=%5Ctextsf%7Bscale%7D+%5C%3B+%28c+%3A+%5Cmathbb%7BR%7D%29+%5C%3B+%28n+%3A+%5B%5Ctextsf%7Babs%7D+%5C%3B+c%5D+%5Cmathbb%7BR%7D%29+%3A+%5Cmathbb%7BR%7D&bg=ffffff&fg=000000&s=0&c=20201002)
for some startup cost 
and 
observations into a replication like combination (
where 
is above 
and 
(partial expressions). Forward slicing preserves meets in the lattice; backward slicing should be consistent and minimal with respect to forward slicing (
and 
which form a Galois connection, i.e., 
. [Given one of the slicings we don’t necessarily get the other for free].
...never odd or even... 