What I Want from a Type System (2016)
gist.github.com
gist.github.com
1 - For each term in the language, there must be an unique "best type" that describes it. (principal type property)
2 - If principal types exist, then you also need to show that a type inference algorithm exists. (decidability of types)
3 - If the type inference algorithm exists, it must execute in a reasonable amount of time
Many of the type system features that one might want to add to a language can violate one of these properties, specially when you start combining them together into a single type system. In particular, subtyping is particularly tricky.
Finally, there is also a problem that you can never get away from with full global type inference schemes: type error messages tend to take the form of "type A is not equal to B" instead of "found type A, expected type B". Then a type constraint cannot be met, the error message cannot tell you which of the two sides is the wrong one. Additionally, the way that type constraints propagate means that the error message might not necessarily point to the true source of the type error.
For these reasons, even in language with full type inference it is usually a good idea to at least have type annotations for top level functions.
Firstly, I wrote this about 3.5 years ago. I was wondering why people were suddenly commenting on it and now it all makes sense.
Part of the fun of writing articles about this is watching everyone argue about what language can be forced into representing types in a given way. Yes, I assume in any situation that if I want a feature X in a type system, that somehow Haskell can be forced to give me that feature, but that doesn't necessarily mean it will fit with the ecosystem of the language or that that's the only feature I'm looking for in the language. So saying "someone hasn't done their homework if they think X can't be done" isn't relevant, what is relevant that I'm not aware of a language that provides the type system features I want combined with acceptable set of trade-offs.
So anyways, I'll stick around for awhile and see if I can answer any questions. Thanks for the discussion, all!
Maybe it's because I'm influenced by C# but viewed from that perspective it would be like requiring you to explicitly declare that e.g. some value is a ProductID but when you're declaring a type you wouldn't need to declare it is a Person, provided it simply implements the right fields (in C# you would have to explicitly implementing some interface to clarify that first-name and last-name do indeed refer to a person and not, for example, the head and tail of a list of names). This does mean that any external code can't implement your interfaces though, which is a bit annoying, though fixable.
I've always appreciated the advantages of code being legible as plain text files. But maybe it is just a little absurd when language design is shaped to fit the desire not to evolve the storage format and editing interface.
The author doesn't make any comment on dispatch let alone multiple dispatch.
They appear to be writing for the kind of quasi-schema'd information bureaucracy that's very important outside of SV. Lots of data in XML that never quite lines up with an object model.
The Haskellite approach would also say that "what operations are available on that thing" is the wrong way round; you define your operation, and the type signature tells you what kind of things will work with it.
Isn't the common case that you already have "the thing", you have a rough idea what should be done, and you want to see what operations/transformations are available? That's when autocomplete and a static type system comes in handy.
Some (more obscure) languages unify this, i.e. f(x) is the same as x.f(). I don't think there's a "wrong way around", the difference is a technicality.
I'm going to (very lightly) push back and say no, I don't think that's the way I want to program. Certainly I've seen functional systems where it's mostly about syntax, but I think there's also a difference here that is more than technicality.
I'm having a hard time thinking more concretely about exactly what it is, but intuitively the statement you made rings a few alarm bells for me.
If so, I'd point out that methods can just be pure functions and objects can be immutable.
Or, more controversially, partial application is just a lazy person's method definition.
This is true, but then you start wondering what the data hiding is for, especially if an object has getters for all its immutable members.
I think it's more about organization? And more about how often structs in my functional systems evolve over the course of a single function call. Maybe it's that when you're attaching methods to an object, you have a finite number of things you can do to that data.
With a struct, I'm always just one `map` (or even a mutation) away from being in a different format that can be consumed by different methods. Of course this can happen with classes as well -- you can have transformation methods, there's nothing technical stopping you from setting up a class system where you're jumping around that much. But I feel like it happens more when I'm doing functional programming.
An IDE that was focused on "what methods can consume this data" might not capture that -- I'm not saying it wouldn't occasionally be useful, it's just that "what methods can consume this" is not the first question I ask when I see a struct. All of the methods consume it, I can just transform the data or combine it with another struct to fit whatever format a method requires.
> Or, more controversially, partial application is just a lazy person's method definition.
I reasonably strongly agree with this.
I know we like to fight here, but I think both are valid approaches. They may correlate with top-down vs bottom-up design, or which side of the API you're designing. If you're consuming an API, yes autocomplete and suggestions are hugely helpful, as is a type system to prevent you passing garbage to the API and having to have it return errors.
The specific use case from the OP:
> Well a lot of work I do has to do with very messy business logic. Situations were a company wants to convert their receipt system, trading engine, or something of that nature into computer code. Often this data is very complex and hard to define. Situations where a importer may bring in 100 fields but we only care about 10. Thus it's often important to require that certain data match a model, but allow for extra data to flow through a system without much effort. In addition, the problem with nominal k/v types is that I often find myself converting between two types simply because function A requires a DBPerson, and function B requires a UIPerson. If the keys and values are the same, they should flow through, while still keeping me from saying PersonName = ProductID.
I can certainly see where they're coming from - they neither need nor want schema enforcement as they have no control over the input data. Most of their types relate to business semantics, but since the semantics are loose it's not suitable to ram everything into a Person object. And certainly in OO-heavy systems you do end up having to convert between similar-but-not-identical objects that were intended to represent the same thing but defined in different systems.
D has this (called Uniform Function Call Syntax (UFCS) ) and also has optional parenthesis for call with no more arguments which turns this:
send(getInvoice(calculatePrice(x)));
into
x.calculatePrice.getInvoice.send;
It also eliminates the need for extension methods since any function that takes any given type as its first argument is automatically callable as if it were a method of that type, this also applies to templates with the type of the first argument determined by a template parameter.
As for a "wrong way around", you can overdo it both ways, use your judgement. I prefer UFCS for more heavily nested calls which you get when you do a while lot of data transformations all in a row. Some times I use it for a single call but not very often.
Flow seems like an interesting package to check out if I ever go and start using Haskell seriously.
My favorite is Elm, which has |> and <| for application, and >> and << for composition, in the intuitive directions. It makes it easy and natural to eta-reduce/expand, when you want to.
Matlab! Which uses a pretty wild form of dynamic dispatch when the (more common) f(x) form is used:
> When MATLAB® invokes an ordinary method that has an argument list, it uses the following criteria to determine which method to call
> The class of the leftmost argument whose class is not specified as inferior to any other argument's class is chosen as the dominant class and its method is invoked.
> If this class does not define the called method, then a function with that name that is on the MATLAB path is invoked.
> If no such function exists, MATLAB issues an error indicating that the dominant class does not define the named method.
Also, it doesn't care at all if you pass in an array or a scalar (everything's an array). Methods must be written to handle a "this" of any size - even empty.
What an odd language.
> The Haskellite approach would also say that "what operations are available on that thing" is the wrong way round; you define your operation, and the type signature tells you what kind of things will work with it.
i'm not sure if i understand. using typeclasses i can define a Haskell function for summing collections:
sum :: (Foldable f, Monoid a) => f a -> a
sum x = foldr (<>) mempty x
> The Haskellite approach that says "what operations are available on that thing" is the wrong way round
which left me pretty confused!
How does code completion work in Haskell IDEs then? It doesn’t seem that it would have a decent anchor.
Outside of the C++/Java/.Net world, names tend to be much smaller.
Anyway, it works like autocompletion works on any textual input, a couple of characters severely restrict the amount of words you are trying to write, and context guides on the rest.
Haskell in particular tends to exhibit local variables that are less than a couple of characters long, so autocomplete does not even make sense for those.
Globals tend to have wither short distinctive names when they are more generic, or long prefixed names when they are concrete. Either way, just completing over a dictionary gets results that are at least as good as you'll get on Java/.Net/C++ IDEs. Haskell also brings a lot of added context, but I don't know of any IDE that uses those for completion (and honestly, I don't miss it).
That has little to do with code completion, which is more about API discovery than saving on typing. It seems like many Haskell enthusiasts never figured that out, so they didn’t bother with it in tool development. Which is funny, given with all that extra strong typing, they might be able to come up with an experience that is much better than the other languages, but I guess not yet.
I'm hopeful that cool type-powered IDE features will start to arrive once haskell-ide-engine is a bit more stable. It's getting there!
There are some pretty awesome IDE ideas in Haskell-ish languages like Idris [1], too. There is some movement towards dependent types in Haskell, so it might get similar features one day.
List.
| length
| hd
| tl
...Case in point, the core toolchain (e.g. the compiler itself) supports "typed holes". Basically, you drop a placeholder somewhere in an expression and the compiler will infer and report the type of the sub-expression. There are also tools to search either within a program/library or e.g. the entirety of the Hackage package database for functions matching a certain type. It seems like a relatively short distance from there to having an IDE or code editor that can list possible expressions/functions that could satisfy a particular placeholder. And to me, having e.g. a list functions that transforms the input(s) I have to the output I need seems much better than e.g. a partial list of all the functions that relate to a particular type.
And maybe such a thing exists today, but I have had really bad luck trying to get Haskell tooling that works well and is easy to set up.
I don't get why this is important. If the original author, you had an idea of what you wanted to do with the thing. As a reader the thing is whatever supports the functions called on it in the body. Naming is important. Adding type annotation for humans is a good pattern and requiring it everywhere as part of language spec doesn't seem beneficial. Heck even Java now has var like js in method bodies.
In fairness this sort of data is metadata that can be added at tooling time - there's no need to place it in the source itself.
Ruby and Python both started as scripting/glue languages meant for small programs. At that scale, it doesn't really matter.
When the codebases they were used for started getting bigger and started having longer histories and a need for refactoring, that's when people started asking for more structure.
Most of things he requested are possible with HList in Haskell. A library, nonetheless. From 2008, I believe.
PS Structural subtyping is tricky: https://pdfs.semanticscholar.org/ff6f/1c49ff00efa483807fae71...
It took quarter of century to get it right. Most probably the author of gist just don't get it's trickyness yet.
Here would be an example of the first case : https://wandbox.org/permlink/AIgZtkFgTuiQReDT
I believe author somehow messed the part where his requirement considers machine representation. This is an implementation detail, BTW. Sometimes it is desirable to have as tight representation as possible, othertimes it is not.
I believe that it is quite possible to have associated type for HList records in the vector package style for unboxed vectors - vector represents array of structures as structure of arrays and for HList we can do something alike. Again, you can have it if you want it.
While I believe those make for a more streamlined language (I do prefer F# to Ocaml), it also means that you regularly need type signature to desambiguate things where nothing was needed in Ocaml.
Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety.
Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort.
[1] https://github.com/davidfstr/idris-insertion-sort/blob/maste...
There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system.
One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map.
[1] https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.
Module X expects the "foo" key, then write a function that checks if it has the foo key and returns a type Maybe(HasFoo). It's less good than just treating the type as the union of HasFoo and HasBar or whatever, but if you fully decouple, then you have to be able to handle the case in which the mapping lacks a foo key anyways, and this will statically froce you to.
Remember, in the sense we are currently talking about[1], objects are untyped, it's variables that are typed. So there is no need to describe the type of this map that is passing around in concrete terms; it's perfectly cromulent to treat the map as a TypeA in one place and a TypeB in another place, so long as you ensure that the prerequisites for those types are satisfied by the object.
It is true that it is usually preferable in statically typed languages to demonstrate that the map satisfies the requirements for TypeA before type erasure (i.e. at compile time), but if you want total decoupling, then that is not possible (since the requirement that the map have keys X and Y would need to be enforced outside of Module A). This does not mean that a type system cannot help you though.
I think we are getting to the limits of what can be easily communicated via HN comments, so if you still don't understand, then perhaps I'll write a blog article explaining it more fully.
For example, there is middleware for parsing our request params into a :params key. There's another piece of middleware that parses the values of these keys. So, you may or may not have a :params key, and the types inside the params can be absolutely anything. Then you could just have completely separate middleware that might add something like a CSRF token to the request map. And so forth. Your only real option here is to treat the entire structure as Any type.
If you still don't understand the problem, I really don't know how else to explain this.
On the other hand, we can easily measure the effects of factors like sleep [2], overwork [3], and happiness [4] on code quality. If static typing was an actual factor, we’d see exactly the same kinds of effects.
There’s nothing wrong with enjoying static typing, but there’s simply no evidence that it plays any role past personal preference. Different people solve problems in different ways, and have different pain points. It's entirely possible that each type discipline appeals to different mindsets. That is a value in itself.
[1] https://arxiv.org/abs/1901.10220
[2] https://arxiv.org/pdf/1805.02544.pdf
[3] http://web.archive.org/web/20090824001133/http://www.curt.or...
[4] http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-...
All I'm saying is that if you forgo static checks to avoid "paying the cost" -- and I do agree they come with a cost -- all you're doing is paying the cost elsewhere. Remember all those people saying "I don't need static types, I just write lots of tests"? That's a cost [1]. Or "I don't need types, I've never had type errors"? That's also a cost, though a more insidious one: ignoring that some of the errors they did get could have been prevented with a use of types they just aren't familiar with.
I'm not arguing that static typing/analysis leads to better quality. I'm arguing that people who don't want to pay its cost actually pay it elsewhere.
To be honest, if pressed I would also argue that I wouldn't want a critical system with the potential to endanger lives to be written in a dynamically typed language. Then again, static types alone wouldn't be suitable either.
----
[1] I knew one guy who didn't write tests either. "I don't need tests because they are a waste of my time: I never make mistakes". Guess where he paid the cost? :P Even then, not even writing tests is also an acceptable tradeoff in some situations!
If you have a specification for what the code is supposed to be doing, and you do specification testing then you will have a high level of confidence regardless of the type discipline. The kinds of errors that will slip through in a dynamic language would necessarily be edge cases and undefined behaviors. These are typically the kinds of bugs that static typing can help you catch.
On the other hand, dynamic typing facilitates features such as hot loading. Just last week my team had a production issue where the service we were using changed the API, and the team managing it didn't notify us. We were able to update the code that talks to the service via the REPL with zero downtime. This is something that would've been a much bigger issue if we had to take the whole system down.
I worked on a research project (a subproject of the project described in this NYT article about Peter Neumann: https://www.nytimes.com/2012/10/30/science/rethinking-the-co...) that experimented with addressing data security and integrity issues using strong types.
For example, writing data to the wrong channel, or reading from the wrong channel, was a type error.
Most of the time, most operations could be statically checked, but sometimes they could not. You might, for example, attempt to send a message to a recipient whose privileges change during transmission. Static checking won't help for such cases; the system needed dynamic checking.
The project used a novel programming language with both static and dynamic typechecking. It specified a hardware platform with tag support for dynamic types.
Mention either static or dynamic typing and a controversy erupts as night follows day between advocates of one and advocates of the other. Why not see the costs and benefits of both? I imagine that the practical answer is that supporting one type discipline costs less in development resources than supporting two, but that doesn't mean that the rejected discipline is therefore wrong and bad.
I liked that the project in question's designers didn't engage in a spurious struggle over static versus dynamic types. They understood that both were valuable, that each offered some benefits that the other didn't, and so they used both.
You need a mix.
Most dynamic types then go on to say why bother at all with static. That's where we disagree. It's dynamic types people that tend to be all or nothing. Where as static type people say use them where it's helps catch the obvious errors, so you don't have to write so many tests.
I also find that runtime contracts as seen in Racket and Clojure provide another interesting approach. From my experience contracts make it much easier to specify actual business constraints.
insert x [] = [x]
insert x (y:ys) = if x > y then y:(insert x ys) else x:y:ys
insertSort xs = foldr insert [] xs
Yes, Idris' proofs are verbose. They're also a perfect validation of the properties that need to be proven, better than any test case in the world.
Unfortunately, Haskell type system can result in baroque code in many cases as well. The whole reason monads are so prevalent in Haskell is due to the fact that the type system tracks side effects. Here's an example of a problem this introduces from the core.async library.
https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg
When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought.
What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency.
In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable.
So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it?
> 1) Full type inference.
Really, while writing and hacking, you want it, but ideally the system should be able to fill in your types for you. Note, though, that there's a tradeoff: the more overloading and other conveniences, the less complete the inference can be.
In the system I'm working on, it's intended to deploy a library + documentation, so all types would be annotated in the artifact generated regardless of whether they are in the source.
> 2). Value types in structures would need to be nominal, not structural.
My answer to this is we want cheap sum types. In Tenet, a sum type can be constructed without any declaration by writing tag~expr. This implicitly defines Union[tag~WhateverExprTypeIs].
Since unions implicitly combine, if I have one branch return meters~55 another can return error~"something broke" and the return type overall is implicitly Union[meters~Integer, error~String].
The idea of declaring that, e.g. meters~X and centimeters~Y are interchangeable representations of the same value is something I'm thinking about; it's getting at a facility for encapsulation.
> 3) Collections of [product types] would need to be inclusively typed, not exclusive.
So, if we have syntax for retrieving an attribute `x.a + x.b` and we know + takes integers, we can deduce an assertion that x is some product type with two integer attributes a and b. I call that an open tuple, as opposed to a closed tuple.
But all product types must be closed (exclusive) in order to construct them, obviously, and for non-dynamic languages, it seems like you're liable to have code size explosion (multiple copies of functions to support each type used) if you allow polymorphism this way.
> 4) ... it would be important to have all these structural members be namespaced as well.
I'm curious what people think the best namespace schemes are, because most of them seem like a lot of complexity for what they do. But...
> 5) Now I would still need basic set logic for these types
It won't make the first cut, but the basic operations would be sum and diff (for sum types), times and project (for product types) and a renaming facility with globbing seems like it might answer #4 just fine.
I’m working on a small language idea right now where I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name (borrowing the rdf model here)
So (n1: v1) might be a value v1 bound to n1. And (n2: v2) another. (n1: v1)(n2: v2) = (n1: v1, n2: v2), and one could even imagine (n1: v1, n2: v2)(n3: n1+n2) as a valid expression. Which of course is equivalent to ( n1: v1, n2: v2, n3: n1+n2, ) not entirely unlike a let-expression
(I’m thinking of unifying terms and types so a lambda would simply be such an expression where v1 and v2 are types)
Oh well just a toy in my head at the moment. Just found it interesting to see similar tag combining semantics.
(As for namespace I was thinking to borrow the plan9 approach of binding things dynamically, using something like Scalas implicits, for evaluation to do a kind of dependency injection thing, but a global lexically scoped tree for typing it)
> Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name
In theory, an integer is just an uncountable enumerated type. I haven't done that to treat it as opaque / atomic, but you could imagine it essentially being 1~~, 2~~, 3~~, etc.
But that might come back if I want to have sane semantics of floats, as in not treating NaN as a magic value that doesn't equal itself.
> I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind.
This might be helpful just as something to think about, but there is already an example of One Structure to Rule Them All: relations from the relational algebra. (You want to consider the mathematical definition; SQL tables break stuff because of legacy.)
A relation can naturally represent any container, but also any function if you allow them to be infinite. So if you have a relation that states all values of y = cos(x), you can join it with an existing expression to apply the `cos` function. (Or `acos` if the system is clever enough.) And that, obviously would get translated into actual function calls.
> So (n1: v1) might be a value v1 bound to n1. ...
I had to read that a couple of times, but I think I get it. I think being able to combine structures makes a lot of sense, and it's one of those ideas that's not implemented in most languages (as the OP mentions) so we people tend to engineer around the lack of it, so it'd be interesting what idioms develop with it.
> As for namespace I was thinking to borrow the plan9 approach
Thanks, I'll have to look into that!
Re: plan9, this is in the context of language I imagine as a kind of interactive environment (think small talk) and where partial evaluation would be the means to construct deployable artifacts. In this environment i expect to support metaprogramming and reflection, typing and unit-tests as something very dynamic and integrated, but purely design time thing. Again, not entierly unlike how you work with a relational dbms system and its schema.
Lately I've even started to even question whether TypeScript is really worth the trouble and slowness it's causing. I wrote about it briefly here:
https://sdegutis.com/2019-06-20-considering-removing-typescr...
On one hand, TypeScript's type system is extremely convenient when mixed with VS Code. On the other hand, it's getting slower and slower, which is making it actually counterproductive. I often wonder if I'd be faster in just plain JS.
This exercise is more similar to converting a typed language like java to a type inferenced one (a la java 12 or "auto" in C++11). If you didnt have the guard rails of types the way you built your system may differ by relying a lot more on runtime behavior and conventions rather than compile time type checking and explicitly enforced rules.
Having written in many statically and dynamically typed languages, I feel like I should have already come to a conclusion by now. Yet somehow I'm still on the fence after all these years.
Also of course any form of runtime type checking is missing.
https://www.se-radio.net/2009/07/episode-140-newspeak-and-pl...
In Go, there's a practice called "microtyping" (credit goes to HN user jerf) where everything is type defined to a semantic name. So you never have a struct with a string for ProductID and ProductName. Instead, you have a struct containing a ProductID and a ProductName. This makes it very easy to change your mind. I used to have a base64 encoded UUID as an EntityID in my MMO. I implemented microtyping, and after that, changing EntityID to 128 bits was a breeze!
It _kind_ of works in typescript, but it's not enforced by tsc. Definitely helps readability, though.
The reasoning behind wanting this is good. It can however be satisfied differently. I find structural typing to be more convenient where I have the ability to define a type for another that is not considered to be equivalent. A good example is how an int can be defined into different types with conversions in Go.
If we were to follow through with nominal typing we would need transforms to rename the same structures when working through abstractions that make sense having different names.
That being said, all these things are implemented in PureScript, I believe.
I have think about this for my toy relational lang, I consider too the best is allow:
fun print(people:People[id, name])...
Plus, re-combining of types is inbuilt. Need to extent person?
rel Customer Person join Address, Phones...The more clever, independent, and unbound you are, the less you appreciate types, because you never really feel the pain points that types alleviate.
(unless he finds splattering `ref` and `copy` (or their syntactic sugar of `&` and `@`) in his code acceptable, in which case, congrats!)