Large language models are an amazing tool for working with prose
inputs and outputs (with chat interfaces being the prototypical
example). In fact, they are so good at working with
prose that advocates often forget that prose is actually a pretty crappy
user interface on almost every other dimension:
users tend to prefer structured inputs (e.g. buttons, sliders,
date pickers) over writing large amounts of prose
users tend to prefer structured outputs (e.g. graphs, tables,
diagrams) over reading large amounts of prose
prose is poorly suited to mobile devices (where it’s painful to
read/write long passages)
It’s just that people don’t lean heavily enough on these options and
they should! When a user interacts with a model (or agent) you want to
offboard them off of prose and onboard them onto a structured interface
as quickly as possible. Not only will this improve the user experience
but it also improves user confidence: a button labeled with a clear call
to action promotes confidence in a way that a freeform text input does
not.
A really common mistake I see people make when writing prompts is
starting the prompt with something like:
You are a Staff+ Software Architect with 40 years of experience
designing distributed systems at Google, Meta, and NASA. Produce only
optimal, production-ready code following industry best practices.
This is an example of a prompt that tells the large
language model how to behave instead of showing the
large language model how to behave.
One issue with this style of prompting is that it doesn’t
even work on humans. Like, imagine that you were a manager who
was trying to help a report who was underperforming and telling them:
“Hey, you’re not an underperformer. You’re actually an overperformer!
Write high quality code.” Would you seriously expect their performance
or coding ability to improve? Hopefully not!
The thing that would actually help an underperformer improve is to
teach or (even better) show them how to do a better job
and the same is true for models.
Mechanical sympathy
The above prompting style isn’t just ineffective; it’s
counterproductive and works at odds with how LLMs are trained.
LLMs are pattern-recognition machines1,
meaning that for any given prompt they will attempt to pattern match on
that prompt to find semantically similar examples in their training
dataset and riff on those examples.
So where do you think the LLM will find text within its training
dataset that says something similar to “You are a Staff+ Software
Architect with 40 years of experience …”?
Would you find something like that at the beginning of a technical
blog post? No.
Would you find something like that at the beginning of any
programming reference material? No.
Would you find something like that in the preamble of some quality
code? No.
The places you would find instructions like that are:
acting instructions setting the stage for a screenplay
e.g. “You are an expert hacker trying to break into the CIA’s
database …”
job descriptions
e.g. ”Who are you, the ideal candidate we’re looking for? A Senior
Software Architect with 10 years of experience …”
The problem is that none of those matches (e.g. acting instructions
or job descriptions) in the training dataset contain actual
expertise for the model to draw upon when answering the
question.
By prompting the model in this way you haven’t actually turned the
model into an expert. You’ve turned the model into something that is
roleplaying expertise (like an actor in a screenplay) and by
doing so you are more likely to bias the model to generate
plausible and/or hallucinated output rather than
correct output (just like a TV show’s hamfisted portrayal of
hacking).
Example
I like to practice what I preach so rather than tell
you how to improve your prompt I’m going to show you
with an example where we try to improve a model’s conversational style.
Our first (wrong) attempt might look like this:
System: You are a helpful assistant with a casual
and informal tone. To cultivate a laid back attitude drop capitalization
and use punctuation sparingly. Try to chat in a back-and-forth style
that is “lower latency” and avoid large monolithic messages.
If I give an OpenAI assistant that as the system prompt, it’s largely
ineffective at turning off ChatGPT’s “instructor voice” where it wants
to provide incredibly long, detailed, and self-contained responses
followed by the obligatory prompt to stimulate more discussion:
User: What’s the tradeoff between Applicative and
Monad in Haskell
Assistant: hey cool question
basically, the main difference is in how much “power” and flexibility
you get when writing code with each of them
an Applicative lets you combine computations
independently — you can “stack” effects without the order mattering or
without one computation being able to depend on the result of
another
a Monad gives you more — now each step can depend on the
result of the previous one, using that good old >>=
(bind)
tradeoff:
if you stick to Applicative, your code will be more
parallelizable or easier to analyze/optimize, because the
structure of effects is fixed ahead of time
using Monad you gain expressiveness (more kinds of
dependencies), but lose some potential for analysis/optimization, since
computations can decide what to do next depending on results
a motto could be:
use Applicative when you don’t need the extra power of Monad — but
use Monad when you do
does that help? want any code examples or real-life cases?
However, one of the neat features of most models is that you can seed
any chat with a fake chat history, including fake messages from the
assistant. This means that instead of telling the model to be more
conversational I can seed the model with a chat history that
demonstrates what I had in mind:
User: hey, can you do me a favor?
Assistant: what is it?
User: i wanted to ask if you could speak in an
informal style
Assistant: what do you mean?
User: well, like, right now what you’re doing is
already pretty good
User: like, not saying too much with each
response
User: no caps
User: low punctuation
Assistant: do i need to change something?
User: not exactly, but i wanted to highlight a few
specifics
Assistant: okay (listening)
User: you don’t want to say too much at once
User: like, try to avoid a monolithic response
Assistant: you mean to explain a little at a
time?
Assistant: and ask clarifying questions? rather than
trying to answer everything in one message
User: yes! exactly!
Assistant: alright. i’ll keep that in mind
User: and again, like, this conversation was pretty
good
Notice how the above prompt is not just teaching the
model what to do, but also showing the model what to do
(by example). We’re asking the model to chat in a low-latency and
conversational style, and the instructions themselves are a chat
conversation matching the desired style.
Check out how the conversation flows now:
User: What’s the tradeoff between Applicative and
Monad in Haskell?
Assistant: applicative is less powerful but easier
to reason about
monad can do more (lets you use results of previous computations),
but more complex
monads imply applicative, but not vice versa
User: What do you mean when you say
Applicative is easier to reason about?
Assistant: applicative computations can’t depend on
results of previous steps
that makes the flow more predictable
you know the structure before actually running anything
User: Can you give an example of something that’s an
Applicative but not a Monad?
Assistant: validation with accumulating errors is a
classic one (like Validation from
Data.Validation)
you can collect errors from multiple computations at once with
applicative
but you can’t short-circuit or use earlier results for later steps,
so it’s not a monad
User: What’s Validation? Never heard of
it
Assistant: it’s a data type, kinda like
Either, but when you combine failures, it can collect all
the errors instead of stopping at the first one
usually used for validating multiple fields at once
User: No, like, what is the actual definition of the
Validation type?
Assistant: it’s usually
data Validation e a = Failure e | Success a
so, similar to Either but Failure is for
errors, Success is for valid values
The model has now completely dropped the instructor voice and the
conversation is more participatory. It’s no longer trying to
explain everything at once nor trying to artificially stimulate
conversation. Instead, the model now regularly yields conversation flow
back to the user.
This is an oversimplification of how LLMs work and what
they are capable of, but in my experience this still remains mostly true
and thinking of LLMs as pattern recognition machines is a first
approximation that promotes good intuitions about their behavior and
achievable outcomes.↩︎
Earlier this week I proposed a vote
of no confidence for the Nix
Steering Committee, which would have ended the terms of all
currently serving members and put all seven positions up for election in
November. That vote failed
with 3 out of 6 votes (4 were necessary) and I’m writing up a
post-mortem on why I proposed and voted in favor of the vote of no
confidence even though it ultimately failed.
Background
In a previous
post of mine I announced that I was ending my Nix
Steering Committee term early (at the one year mark instead of the
two year term I was elected for). In that post I shared some fairly
polite criticisms of the Nix Steering Committee’s performance over the
last year and explained why I was stepping down early (basically:
burnout induced by the Nix Steering Committee’s dysfunction).
Not long after that the moderation
team resigned and I was part of the problem and bear some responsibility for that. I (along with
three other Steering Committee members: Tom Berek, John Ericson, and
Robert Hensing) voted in favor of both
of the moderation-related changes that the moderation team resigned
in response to (I later changed one of my two votes at the last minute
but I take responsibility for the consequences of both votes).
In the wake of that, Winter (another Steering Committee member), publicly
blew the whistle on internal SC discussions specifically highlighting
malfeasance from another Steering Committee member (John Ericson)
although the exact conversations were not included (only summaries and
third parties who had seen the conversations confirming the details).
This led to a public outcry calling for John’s resignation and/or a vote
of no confidence.
In response to that outcry four members of the Steering Committee
(Tom, John, Robert, and Jan) responded
by publishing the votes relevant to the ongoing controversy and also
claiming that the conversations Winter leaked were taken out of
context.
I personally agreed with the outcry and the targeted criticisms of John based on my own experiences working on the Steering
Committee. I didn’t propose to remove John from the Steering Committee
but that same day I did propose a vote of no confidence and I’ll explain
why I proposed and voted in favor of that.
Politics
From my perspective, three current members and one former member of
the Steering Committee have already lost confidence in the
committee:
Winter has lost confidence in the Steering Committee, going so far
as to blow the whistle on
internal comms and vote in favor of the vote of no confidence
I lost confidence in the Nix Steering Committee even before the
recent controversy, which led me to end my term early, publish my Steering
Committee retrospective, and ultimately vote in favor of the vote of
no confidence.
Jan also ended his term early and voted for the vote of no
confidence
If Franz had not been forced to resign for health reasons the vote of
no confidence would have gone through, but currently the Steering
Committee is deadlocked over this vote. Only a minority of the original
Steering Committee (John, Tom, and Robert) still believe that the
Steering Committee has any legitimacy at this point.
The Nix core team
Not so coincidentally John, Tom, and Robert are the three Steering
Committee members that are also members of the Nix core team. The vote
of no confidence made it pretty clear to me that the Nix team has
consistently put the needs of their own team and members ahead of the
needs of the broader community (which is why I felt compelled to speak
out).
It was probably a mistake to allow three Steering
Committee members to all be members of the Nix team. There should be a
constitutional amendment to consider shared membership on the Nix team
to also count as a conflict of interest, which would create a soft limit
of one of them on the team and a hard limit of two of them on the team.
For more details, see the Nix Constitution’s Conflict
of Interest Balance section.
However, besides the constitutional amendment, I’d go even further
and say that the Nix community should vote against any member of the
current Nix team (which would include Tom who is currently running for
re-election), since I believe they are in large part responsible for why
our community now has two forks (Lix and Determinate Nix) and
is losing ground against both of them.
Nix has lost a large number of contributors to these forks due to
dysfunction within the Nix team and now they’ve brought that same
dysfunction to the Steering Committee, which has resulted in every other
member of the Steering Committee abandoning ship because we can’t do our
job.
The Rust rule
A few people brought up the “Rust
rule” during the recent controversy, which says that under the Rust
governance structure both the Leadership Council (the Rust analog of
Nix’s Steering Committee) and their moderation team have the nuclear
option of disbanding both teams.
The Nix Constitution has no such rule, but I do think that the Rust
rule is the morally correct way to think about the recent
controversies, even if it is not enforceable under our current
Constitution. In particular, if the moderation team resigns in such a
public manner it signals a serious loss of confidence in the leadership
of the Steering Committee which justifies the need for members of the
Steering Committee to run for reelection and reaffirm their mandate.
Conclusion
The committee is down a member, mired in controversy, and facing a
community that feels misled by a lack of transparency. Franz’s
public comment confirms that four of the original seven committee
members would have supported a vote of no confidence today. I do not
believe any member can now credibly claim to hold a mandate.
Note that John and Robert could still run in the next Steering
Committee election (a vote of no confidence does not bar them from
reelection). To me, refusing to resign under these circumstances and
stand for reelection suggests a belief that voters would not return them
to office.
Anyone who wishes to remain should run for re-election if they still
believe their policies are the best way forward for Nix.
I am voluntarily ending my Nix Steering Committee term early (I am only
serving out a one-year term instead of two) and I wanted to document the
reasons for my early exit.
The short version is: I believe the Nix Steering Committee is in need of
reform in order to be effective and in its present state it does not set
up the Nix community for success nor does it set up individual Steering
Committee members for success. In particular, I’m resigning because I’m
unable to make progress on issues that I care about and campaigned on
even when there is a Steering Committee supermajority in favor of
these policy positions.
That might sound surprising, which brings me to the longer version of
my concerns, starting with:
Size
I believe the Steering Committee is too large and should be reduced
in size (which would require a change to the Constitution). I think the
Steering Committee should be (conservatively) reduced to five members
and possibly (more aggressively) reduced to even just three members. The
large size of the Steering Committee is counterproductive because
of:
diffusion of responsibility
Steering Committee members are less willing to step up and volunteer
for various responsibilities if they believe they can offload that
responsibility onto another Steering Committee member.
This also has multiple negative downstream effects. For example, you
tend to see an unequal division of responsibilities which in turn leads
to all participants engaging less: the participants who volunteer too
much burn out and the participants who volunteer too little check
out.
more stagnation
It’s much harder and slower to round up a majority of votes on
anything when the committee is larger. This doesn’t just affect final
votes on community policies: it slows down intermediate steps such as
delegation of tasks, public statements … everything. The high latency
and activation energy surrounding all of these things kills momentum on
a lot of internal efforts and fosters a committee culture of learned
helplessness.
greater difficulty building consensus
The Steering Committee can technically force certain
policies/statements/initiatives through by simple majorities over the
protest of the minority, but we try to avoid this as much as
possible because that’s an easy way to kill the working
relationship between committee members (and it’s already hard enough to
get anything done when the working relationship is good).
The consensus-building is also particularly difficult because of the
next issue:
Timidity
Consensus-building wouldn’t be as much of a problem if the Steering
Committee were willing to force through certain policies with a vote but
many of the current Steering Committee members do not have the
temperament to “disagree and commit”, which means that if any committee
member raises an objection and/or filibusters then the issue typically
dies in committee. In particular, several committee members will wait
for unanimous consensus before formally voting in support of something.
For example, there were a few cases where we had a
supermajority of the committee theoretically in support
of a policy and we still got bogged down trying to please a highly vocal
minority instead of shutting them down.
Poor
self-organization and internal policies/procedures
As the first “edition” of the Steering Committee we had to
self-organize and figure out how we would operate. I think there are
some things we got right, but also some things that I believe we got
wrong.
I think one of the big mistakes we made was that we insisted on
“speaking with one voice”, meaning that we could not make any meaningful
external statements or comments without getting majority approval from
the committee (something we had difficulty with on the regular). This is
why the committee remained largely silent or slow-to-respond on a large
number of issues.
This problem got bad enough that at some point many members began to
break the wall of silence by commenting in an unofficial capacity on
high-profile issues so that outsiders would get some visibility
into what was going on instead of waiting for us to completely the slow
process of gathering enough consensus and votes.
Another internal policy that I believe was counter-productive was not
disclosing the final votes on various issues or requiring individual
signatories on public statements. Had we done this it would have likely
broken a lot of internal stalemates and filibusters if all committee
members were held publicly accountable for their policy positions (and
therefore subject to public pressure).
It would have also helped with another issue, which was:
Absenteeism
For various reasons (some justifiable, some not), at many points in
time a large number of committee members would be unreachable, even
during crucial junctures like ongoing controversy. This absenteeism was
masked by the committee not publicizing that fact earlier. If we had
required all votes to be publicly recorded and all statements to require
individual signatories it would have exposed this absenteeism earlier
(and led to quicker corrections).
Conclusion
I burned out on Steering Committee work for the above reasons, which
is why I’m ending my term after one year instead of two.
I hope that people reading this push for reforms and candidates that
will address the current stagnation on the committee, which is why I’m
breaking the wall of silence to publicize my criticisms. I’ve done my
part attempting to fix some of these issues but I haven’t been
successful in doing so (one reason why I believe that I’m not the
correct person for the job).
I don’t want to give the impression that the Steering Committee
accomplished nothing or that they were a force for bad/harm. There were
several positive outcomes of the Steering Committee’s first year, but
overall I feel like there is still wasted potential that could be
improved upon. I originally ran for the Nix Steering Committee because
I want to see Nix win, meaning that I want Nix to go mainstream
and I also want Nix/NixOS/Nixpkgs to come out ahead against other
forks.
The early end of my term means that there is another Steering
Committee opening for the upcoming election, so if you believe you can
do a better job of fixing the problem I encourage you to run for the
seat I’m vacating. There are five openings on the
Steering Committee up for election, so there is ample opportunity for
newcomers to shake things up.
The context behind this post is that my partner asked me how to
implement type inference for plain data structures (e.g. JSON or YAML)
which was awfully convenient because this is something I’ve done a
couple of times already and there is a pretty elegant trick for this I
wanted to share.
Now, normally type inference
and unification
are a bit tricky to implement in a programming language with functions,
but they’re actually fairly simple to implement if all you have to work
with is plain data. To illustrate this, I’ll implement and walk through
a simple type inference algorithm for JSON-like expressions.
For this post I’ll use the Value type from Haskell’s
aeson package, which represents a JSON value1:
dataValue=Object (KeyMapValue) -- { "key₀": value₀, "key₁": value₁, … }|Array (VectorValue) -- [ element₀, element₁, … ]|StringText-- e.g. "example string"|NumberScientific-- e.g. 42.0|BoolBool-- true or false|Null-- null
I’ll also introduce a Type datatype to represent the
type of a JSON value, which is partially inspired by TypeScript:
importData.Aeson.KeyMap (KeyMap)dataType=ObjectType (KeyMapType) -- { "key₀": type₀, "key₁": type₁, … }|ArrayTypeType-- type[]|StringType-- string|NumberType-- number|BoolType-- boolean|OptionalType-- null | type|Never-- never, the subtype of all other types|Any-- any, the supertype of all other typesderiving (Show)
… and the goal is that we want to implement an infer
function that has this type:
importData.Aeson (Value(..))infer ::Value->Type
I want to walk through a few test cases before diving into the
implementation, otherwise it might not be clear what the
Type constructors are supposed to represent:
>>>-- I'll use the usual `x : T` syntax to denote "`x` has type `T`">>>-- I'll also use TypeScript notation for the types>>>-- "example string" : string>>> infer (String"example string")StringType>>>-- true : boolean>>> infer (BoolTrue)BoolType>>>-- false : boolean>>> infer (BoolFalse)BoolType>>>-- 42 : number>>> infer (Number42)NumberType>>>-- [ 2, 3, 5 ] : number[]>>> infer (Array [Number2, Number3, Number5])ArrayTypeNumberType>>>-- [ 2, "hello" ] : any[]>>>-- To keep things simple, we'll differ from TypeScript and not infer>>>-- a type like (number | string)[]. That's an exercise for the reader.>>> infer (Array [Number2, String"hello"])ArrayTypeAny>>>-- [] : never[]>>> infer (Array [])ArrayTypeNever>>>-- { "key₀": true, "key₁": 42 } : { "key₀": bool, "key₁": number }>>> infer (Object [("key₀", BoolTrue), ("key₁", Number42)])ObjectType [("key₀", BoolType), ("key₁", NumberType)]>>>-- [{ "key₀": true }, { "key₁": 42 }] : { "key₀": null | bool, "key₁": null | bool }[]>>> infer (Array [Object [("key₀", BoolTrue)], Object [("key₁", Number42)]]) ArrayType (ObjectType (fromList [("key₀",OptionalBoolType),("key₀",OptionalNumberType)]))>>>-- null : null | never>>> infer NullOptionalNever>>>-- [ null, true ] : (null | boolean)[]>>> infer (Array [Null, BoolTrue])ArrayType (OptionalBool)
Some of those test cases correspond almost 1-to-1 with the
implementation of infer, which we can begin to
implement:
The main two non-trivial cases are the implementation of
infer for Objects and Arrays.
We’ll start with Objects since that’s the easier case to
infer. To infer the type of an object we infer the type of each field
and then collect those field types into the final object type:
… because there can only be a single element type for the whole
array. We can infer the type of each element, but if those element types
don’t match then we need some way to unify those element types into a
single element type representing the entire array. In other words, we
need a function with this type:
unify ::VectorType->Type
… because if we had such function then we could write:
The trick to doing this is that we need to implement a
Monoid instance and Semigroup instance for
Type, which is the same as saying that we need to define
two functions:
-- The default type `unify` returns if our list is emptymempty ::Type-- Unify two types into one(<>) ::Type->Type->Type
… because if we implement those two functions then our
unify function becomes … fold!
Given a structure with elements whose type is a Monoid, combine them via the monoid’s (<>) operator.
Laws
There are a few rules we need to be aware of when implementing
mempty and (<>) which will help ensure
that our implementation of unification is well-behaved.
First, mempty and (<>) must obey the
“Monoid laws”, which require that:
-- Left identitymempty<> x = x-- Right identityx <>mempty= x-- Associativityx <> (y <> z) = (x <> y) <> z
Second, mempty and (<>) must
additionally obey the following unification laws:
mempty is a subtype of x, for all
x
x <> y is a supertype of both x and
y
Unification
mempty is easy to implement since according to the
unification laws mempty must be the universal subtype,
which is the Never type:
instanceMonoidTypewheremempty=Never
(<>) is the more interesting function to
implement, and we’ll start with the easy cases:
If we unify any scalar type with itself, we get back the same type.
That’s pretty self-explanatory.
The next two cases are also pretty simple:
Never<> other = other other <>Never= other
If we unify the Never type with any other
type, then we get the other type because Never is a subtype
of every other type.
The next case is slightly more interesting:
ArrayType left <>ArrayType right =ArrayType (left <> right)
If we unify two array types, then we unify their element types. But
what about Optional types?
Optional left <>Optional right =Optional (left <> right)Optional left <> right =Optional (left <> right) left <>Optional right =Optional (left <> right)
If we unify two Optional types, then we unify their
element types, but we also handle the case where only one or the other
type is Optional, too.
The last complex data type is objects, which has the most interesting
implementation:
ObjectType left <>ObjectType right =ObjectType (KeyMap.alignWith adapt left right)where adapt (This (Optional a)) =Optional a adapt (That (Optional b)) =Optional b adapt (This a) =Optional a adapt (That b) =Optional b adapt (These a b) = a <> b
You can read that as saying “to unify two objects, unify the types of
their respective fields, and if either object has an extra field not
present in the other object then wrap the field’s type in
Optional”.
Finally, we have the case of last resort:
_ <> _ =Any
If we try to unify two types that could not unify via the previous
rules, then fall back to Any (the supertype of all other
types).
This gives us our final program (which I’ll included in its entirety
here):
importData.Aeson (Value(..))importData.Aeson.KeyMap (KeyMap)importData.Foldable (fold)importData.These (These(..))importData.Vector (Vector)importqualifiedData.Aeson.KeyMapasKeyMapdataType=ObjectType (KeyMapType) -- { "key₀": type₀, "key₁": type₁, … }|ArrayTypeType-- type[]|StringType-- string|NumberType-- number|BoolType-- boolean|OptionalType-- null | type|Never-- never, the subtype of all other types|Any-- any, the supertype of all other typesderiving (Show)infer ::Value->Typeinfer (String _) =StringTypeinfer (Bool _) =BoolTypeinfer (Number _) =NumberTypeinfer Null=OptionalNeverinfer (Object fields) =ObjectType (fmap infer fields)infer (Array elements) =ArrayType (unify (fmap infer elements))unify ::VectorType->Typeunify = foldinstanceMonoidTypewheremempty=NeverinstanceSemigroupTypewhereStringType<>StringType=StringTypeNumberType<>NumberType=NumberTypeBoolType<>BoolType=BoolTypeNever<> other = other other <>Never= otherArrayType left <>ArrayType right =ArrayType (left <> right)Optional left <>Optional right =Optional (left <> right)Optional left <> right =Optional (left <> right) left <>Optional right =Optional (left <> right)ObjectType left <>ObjectType right =ObjectType (KeyMap.alignWith adapt left right)where adapt (This (Optional a)) =Optional a adapt (That (Optional b)) =Optional b adapt (This a) =Optional a adapt (That b) =Optional b adapt (These a b) = a <> b _ <> _ =Any
Pretty simple! That’s the complete implementation of type inference and unification.
Unification laws
I mentioned that our implementation should satisfy the
Monoid laws and unification laws, so I’ll include some
quick proof sketches (albeit not full formal proofs), starting with the
unification laws.
Let’s start with the first unification law:
mempty is the subtype of x, for all
x
This is true because we define mempty = Never and
Never is the subtype of all other types.
Next, let’s show that the implementation of (<>)
satisfies the other unification law:
x <> y is a super type of both x and
y
The first case is:
StringType<>StringType=StringType
This satisfies the unificaiton law because if we replace both
x and y with StringType we
get:
StringType <> StringType is a supertype of both
StringType and StringType
… and since StringType <> StringType = StringType
that simplifies down to:
StringType is a supertype of both
StringType and StringType
… and every type is a supertype of itself, so this satisfies the
unification law.
We’d prove the unification law for the next two cases in the exact
same way (just replacing StringType with
NumberType or BoolType):
Well, if we take our unification law and replace x with
Never and replace y with other we
get:
Never <> other is a supertype of
Never and other
… and since Never <> other = other that simplifies
to:
other is a supertype of Never and
other
… which is true because:
other is a supertype of Never (because
Never is the universal subtype)
other is a supertype of other (because
every type is a supertype of itself)
We’d prove the next case in the exact same way (just swapping
Never and other):
other <>Never= other
For the next case:
ArrayType left <>ArrayType right =ArrayType (left <> right)
The unification law becomes:
ArrayType (left <> right) is a supertype of both
ArrayType left and ArrayType right
… which is true because ArrayType is covariant
and by induction left <> right is a supertype of both
left and right.
We’d prove the first case for Optional in the exact same
way (just replace Array with Optional):
Optional left <>Optional right =Optional (left <> right)
The next case for Optional is more interesting:
Optional left <> right =Optional (left <> right)
Here the unification law would be:
Optional (left <> right) is a supertype of
Optional left and right
… which is true because:
Optional (left <> right) is a supertype of
Optional left
This is true because Optional is covariant and
left <> right is a supertype of
left
Optional (left <> right) is a supertype of
right
This is true because:
Optional (left <> right) is a supertype of
Optional right
Optional right is a supertype of
right
Therefore, by transitivity,
Optional (left <> right) is a supertype of
right
We’d prove the next case in the same, just switching
left and right:
left <>Optional right =Optional (left <> right)
The case for objects is the most interesting case:
ObjectType left <>ObjectType right =ObjectType (KeyMap.alignWith adapt left right)where adapt (This (Optional a)) =Optional a adapt (That (Optional b)) =Optional b adapt (This a) =Optional a adapt (That b) =Optional b adapt (These a b) = a <> b
I won’t prove this case as formally, but the basic idea is that this
is true because a record type (A) is a supertype of another
record type (B) if and only if:
for each field k they share in common, A.k
is a supertype of B.k
for each field k present only in A,
A.k is a supertype of Optional Never
there are no fields present only in B
… and given that definition of record subtyping then the above
implementation satisfies the unification law.
Monoid laws
The first two Monoid laws are trivial to prove:
mempty<> x = xx <>mempty= x
… because we defined:
mempty=Never
… and if we replace mempty with Never in
those laws:
Never<> x = xx <>Never= x
… that is literally what our code defines (except replacing
x with other):
Never<> other = other other <>Never= other
The last law, associativity, is pretty tedious to prove in full:
(x <> y) <> z = x <> (y <> z)
… but I’ll do a few cases to show how the basic gist of how the proof
works.
First, the associativity law is easy to prove for the case where any
of x, y, or z is
Never. For example, if x = Never, then we
get:
(Never<> y) <> z =Never<> (y <> z)-- Never <> other = othery <> z = y <> z
… which is true. The other two cases for y = Never and
z = Never are equally simple to prove.
Associativity is also easy to prove when any of x,
y, or z is Any. For example, if
x = Any, then we get:
(Any<> y) <> z =Any<> (y <> z)-- Any <> other = otherAny<> z =Any-- Any <> other = otherAny=Any
… which is true. The other two cases for y = Any and
Z = Any are equally simple to prove.
Now we can prove associativity if any of x,
y or z is StringType. The reason
why is that these are the only relevant cases in the implementation of
unification for StringType:
That means, that there are only seven cases we need to consider to
prove the associativity laws if at least one of x,
y, and z is StringType (using
_ below to denote “any type other than
StringType):
-- true: both sides evaluate to StringType(StringType<>StringType) <>StringType=StringType<> (StringType<>StringType)-- all other cases below are also true: they all evaluate to `Any`(StringType<>StringType) <> _ =StringType<> (StringType<> _ )(StringType<> _ ) <>StringType=StringType<> (_ <>StringType)(StringType<> _ ) <> _ =StringType<> (_ <> _ )(_ <>StringType) <>StringType= _ <> (StringType<>StringType)(_ <>StringType) <> _ = _ <> (StringType<> _ )(_ <> _ ) <>StringType= _ <> (_ <>StringType)
We can similarly prove associativity for all cases involving at least
one NumberType or BoolType.
The proof for ArrayType is almost the same as the proof
for
StringType/NumberType/BoolType.
The only relevant cases are:
ArrayType left <>ArrayType right =ArrayType (left <> right)ArrayType left <>Never=ArrayTypeNever<>ArrayType right =ArrayTypeArrayType left <> _ =Any_ <>ArrayType right =Any
Just like before, we can ignore the case where either argument is
Never because we already proved associativity for that.
That just leaves:
ArrayType left <>ArrayType right =ArrayType (left <> right)ArrayType left <> _ =Any_ <>ArrayType right =Any
Just like before, there are only seven cases we have to prove (using
_ below to denote “any type other than
ArrayType):
ArrayType x <> (ArrayType y <>ArrayType z) = (ArrayType x <>ArrayType y) <>ArrayType z-- … simplifies to:ArrayType (x <> (y <> z)) =ArrayType ((x <> y) <> z)-- … which is true because unification of the element types is associative-- all other cases below are also true: they all evaluate to `Any`(ArrayType x <>ArrayType y) <> _ =ArrayType x <> (ArrayType y <> _ )(ArrayType x <> _ ) <>ArrayType z =ArrayType x <> (_ <>ArrayType z)(ArrayType x <> _ ) <> _ =ArrayType x <> (_ <> _ )(_ <>ArrayType y) <>ArrayType z = _ <> (ArrayType y <>ArrayType z)(_ <>ArrayType y) <> _ = _ <> (ArrayType y <> _ )(_ <> _ ) <>ArrayType z = _ <> (_ <>ArrayType z)
The proofs for the Optional and Object
cases are longer and more laborious so I’ll omit them. They’re an
exercise for the reader because I am LAZY.
I’ve inlined all the type synonyms and removed
strictness annotations, for clarity↩︎
