u/mttdin r/ProgrammingLanguages • Recommends
Bidirectional Type Checking - C◦mp◦se 2019 - David Christiansen
0:00 / 0:00
#bidirectionaltypechecking#typeinference#dependenttypes
Bidirectional Type Checking
Compose Conference
2.9K subscribers • 30 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by David Christiansen
Intermediate. Assumes working knowledge.
8.5K views7 years ago1 recommendation
Programming languagesComputer scienceLanguage design and type systemsCompilers and interpreters
David Christiansen explains the history, mechanics, and benefits of bidirectional type checking for implementing robust type systems.
Compose NYC 2019 Speaker: David Christiansen When implementing a type checker, one must answer two questions: how to compare types for sameness, be it a subsumption check for subtyping, a unification algorithm for type inference, or normalization for dependent types, and when to check for sameness. The way most type systems are written provides little guidance on this question. One solution to the problem is bidirectional type checking, in which the typing judgment is split into two modes, one that checks an expression against a given type, and one that concocts a type for an expression. Bidirectional type checking tends to require a relatively low burden of annotations, it scales to powerful type systems, and it tends to do a good job associating type errors with source locations. I’ll discuss the history of bidirectional type checking, show how to bidirectionalize known type systems, and walk through some implementations.Why it's here
1 person recommends thisMoments people linked to
u/Disjunction181in r/ProgrammingLanguages • Mentions
On “Algorithms for typechecking untagged unions, intersections, and dependent types?”
With the first two you generally don't try for full inference, and the latter you don't have a choice. But, I'll bring up inference with subtyping anyway:
You can handle TypeScript-esque union and intersection types using algebraic subtyping (read: alien technology) approaches, one such approach is mlstruct (it is rather technical and I would recommend reading previous approaches by the author to understand it) which uses boolean-algebra backed algebraic subtyping for full type inference here, including also negation types, and allowing for an open-world assumption. I don't think complete versions of these systems can avoid being exponential to check due to the ability to essentially encode…
u/gelisamin r/haskell • Mentions
On “Is there a standardized programming model to build compilers with Haskell that I can follow to assure the best results?”
> Is there a standardized programming model to build compilers with Haskell
Gabriella Gonzles's Fall-from-Grace is intended to be a demonstration of best practices when implementing a language in Haskell. If you were starting a brand new project, I would recommend to fork it and to gradually modify the Grace language into your language, but since you've already started, I recommend to look at the code for inspiration instead.
> So my question is: we already have stateful monads and parsers like parsec as an architectural model to implement the syntax analysis ...
Looking up "syntax analyzis", I see that "Syntax Analysis is a second phase of the compiler design process in which the given…
u/ysangkokin r/haskell • Mentions
On “Where to start learning about type checking?”
Why learn Hindley-Milner when you can learn Bidirectional Type Checking?
This presentation has some references at the end (starts at 39m10s), and /u/davidchristiansen claims that Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism handles Haskell, but is simultaneously way easier than "most other approaches".
On the slides after the references, Bidirectional Type Checking is claimed to "scale way beyond what something like Hindley-Milner can do".
My worry is that Hindley-Milner needs so many adaptations to become compatible with modern Haskell that it might not be the best starting point.
u/bjzabaPikelet, Unnamed Binary DDLin r/ProgrammingLanguages • Mentions
On “Typing the empty list”
> there is an expression which does not have a unique type
So it seems like you have some function like this in your type checker (with better error reporting of course):
/// Synthesize the type of a term.
fn synth(context: &Context, term: &Term) -> Option<Type> {
match term {
Term::Var(name) => context.get_ty(name),
// Check that each element of the list is of the same type, returning `None` if it is empty.
Term::List(elems) => {
let mut elem_ty = None;
for elem in elems {
let next_elem_ty = synth(context, elem_ty)?;
match &elem_ty {
None => e…
u/superstar64in r/ProgrammingLanguages • Mentions
On “Does anyone know of resources or languages which involve inferring types from function behavior?”
Are you sure you want you assigning to change the type of a variable? That seems like i'll open a can of worms to me.
Anyway, if your not familiar with it yet, I recommend you learn about hindley milner type inference and bidirectional type inference. These are the most common ways(as far as I know) of doing type inference in functional languages.
Here's some videos I recommend watching:
* Hindley Milner: link to this video
* Bidirectional: link to this video
u/oa74in r/ProgrammingLanguages • Mentions
On “Any papers/ideas/suggestions/pointers on adding refinement types to a PL with Hindley-Miller like type system? ”
as others have mentioned, bidirectional type checking is a good direction here.
I highly recommend David Thrane Christiansen's primer on the topic: [video
u/sebamestrein r/ProgrammingLanguages • Mentions
On “Good textbook with implementations of OO type system?”
Not really. Bidirectional typechecking usually necessitates some type annotations (like function arguments), but it's reasonably simple, fairly principled, and quite hackable.
Here is a cool video about it
link to this video
u/Roboguy2in r/ProgrammingLanguages • Mentions
On “Questions About Custom Types”
>Well, the derivation of `~A` from `~~~A` is a theorem of intuitionistic logic. It's just double negations that don't derive assertions.
Ah, right. I wasn't thinking here.
> The thrust of the move would be to treat conditional statements as a sequent that execute on true, do not execute (and allow else) on false and throw an error if the evaluation couldn't resolve either way.
Is the idea that there is some kind of proof search happening where it looks at all (some?) of the things in scope to see whether it can use them to derive a `true` or a `false` for the logical expression in question? That makes me think a bit of automated theorem provers. Even more specifically, it makes me think o…