> So, a good place to try and understand underlying linguistic structure is informal mathematics, something he studied in his 1993 paper Type theory and the informal language of mathematics. This investigates both directions of the passage between formal and informal mathematics: sugaring and formalization.
Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation:
- There is a variable called `x` in scope.
- `x` is known to have type `A`.
- `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this.
Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.
Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.
Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums
And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof.
It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs.
> I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course.
A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations?
They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
It was not strictly a logic class, but more of an overview course of discrete math, logic and proofs, and some statistics. They taught -> I think.
I've never heard of "sequent calculus" before, and I don't expect anyone I know to have heard it. Apparently it's not calculus.
> They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
I don't think universities are watered down because they don't teach notation that most people don't know and find obscure. My university is famous for a difficult admissions process, tough courses that most people only learn 2/3 of the material, and grading curves calibrated so getting 60% on exams is enough for a B or A.
Wikipedia says "Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments."
I didn't learn "every statement is conditional" logic involving turnstiles, I learned something where the assumptions were given in the problem, and each line was proven based on the previous lines, which boiled down to the initial givens.
Just in case you're wondering if it's just you: no it's not. PL theory seems almost deliberately designed to make even the most mundane things insanely complicated and difficult to formulate or parse. I'm convinced much of the complexity is absolutely unwarranted and only serves to gate the field to newcomers. It makes things so much more painful than they need to be and turns what could be otherwise a potentially interesting topic into something that's more dry than cardboard.
Most of the notation was invented either before or at the dawn of the computer age.
It's also not particularly difficult to pick up. We teach basic sequent calculus proofs to high schoolers in our summer program. If you can follow the two column proofs from high school geometry, then you can follow the notation used in standard programming language texts and papers.
Mathematics does have a notation problem, and that means you effectively have to learn a foreign language to be able to understand it. And like foreign languages, learning it outside of a structured, classroom environment can be difficult to sustain. Even worse is the fact that while terminology like "monad" can easily be searched for to find its definition [1], how is one supposed to search for ℜ?
Dismissing this foreign language aspect as easy to learn doesn't get to the heart of the matter. Is it really too much to be ask to be taught in vernacular English rather than foreign Church Latin, er, Mathematical Notation?
[1] Assuming that you don't get an answer like "a monad is a monoid in the category of endofunctors," which unfortunately does tend to be the case for higher mathematical concepts.
An opinion that’s largely held by programmers and not people who actually do maths. You learn the symbols and notation as you go and it very quickly becomes understandable. I certainly Duns I have less issues understanding mathematical notation than I do reading some programming languages.
> how is one supposed to search for ℜ?
That’s chalkboard R, represents the real numbers. Searching “fancy R mathematics” (in Duck duck go) nets a page that explains what the chalkboard R, N, P, Q and C symbols all mean.
> Is it really too much to be ask to be taught in vernacular English
Mathematical texts used to be written in plain English without the notation, it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
> An opinion that’s largely held by programmers and not people who actually do maths.
The "people who actually do maths" will almost by definition exclude anyone who has issues understanding the notation. You need to look at the latter group of people to work out if the notation is unnecessarily obtuse.
> it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
As a counterexample, consider the proof that undirected Hamiltonian cycles is NP-complete, by reduction from directed Hamiltonian cycles. Karp's original paper says literally just this:
N = V × {0, 1, 2}
A = {{<u,0>, <u,1>}, {<u,1>, <u,2>} | u ∈ V} ∪ {{<u,2>,<v,0>} | <u,v> ∈ E}
By contrast, a vernacular English description would look like this:
Replace every node in the directed graph with a set of three nodes in a line. Gather all the incoming edges to the first node, and all the outgoing edges to the last node. Every path that visits every node exactly once must reach the middle node by starting at the first node and going through to the last node, and thence to the first node of a corresponding subsequent node, so every Hamiltonian path in the undirected graph is a Hamiltonian path in its directed counterpart.
Vernacular English isn't capable of describing some concepts succinctly enough to be useful to mathematicians. If English was superior people would be using it.
This 'argument' always just seems to be a thinly veiled excuse to avoid putting in the bare minimum effort required to understand a complicated topic.
> Most of the notation was invented either before or at the dawn of the computer age.
I mean, what's why I said almost?
> It's also not particularly difficult to pick up.
Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.
Our highschoolers pick it up just fine, and are building complicated proofs within 3 lessons. That's not intended as any sort of attack, but it does make it hard for me to believe that the notation is particularly difficult to learn.
Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list.
And there's really no way to study something like type systems without inventing some sort of notation.
You can go back and read early papers in mathematical logic before the notation was invented.
They take pages upon pages to communicate very simple things.
So are you really telling me your high schoolers would've had no trouble with this [1] (pages 52, 58, etc.)? How do you think the average CS student would fare? Is this kind of notation genuinely as intuitive to you as other mathematical notation? My brain takes like O(n^3) to read this stuff and it's not the first time it's doing it either.
For the record: I am a high school senior who learned about type theory in my free time. When I make this comment, I do not mean to boast, and I did invest a lot of time into learning TT.
It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules.
The top-left rule on page 52 says that given that:
- In context Gamma, T1 = T2 where both have kind *
- If x : T1 is added to the context Gamma, K1 = K2
you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2.
A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used.
The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).
I appreciate that you're trying to help but I'm confused why you're constantly trying to explain the notation to me. I'm not saying I never understood the notation, I'm saying I very much did study and understand it, and found it incredibly convoluted, unintitive, unwarranted, and painful to deal with.
Sorry. For me, when I see the rules, I just scan over them and figure out what it says. I think it just comes from seeing the notation many times - I guess when I first came across the notation (when learning about Hindley-Milner) it was completely foreign to me, but now I can recognize common patterns:
Gamma |- exp : A
This is a common pattern that says that exp has type A when the contents of Gamma are in scope.
Gamma |- exp1 = exp2 : A
This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope.
I've found that most type system rules follow the same format more or less.
Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)
-> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.
I mean, yeah? I think you were trying to give an example of a hard to understand notation, but that page is relatively straightforward and concise. In fact, I can't think of a more straightforward (and non-ambiguous) way to express those concepts.
Frankly, I'd expect any CS student at a decent university to be able to parse that page fairly easily.
I completely sympathize with the difficulty in understanding the notation and wish it were more accessible. I struggled with it for some time. But as someone who eventually learned it, I find it to be fairly sensible. What would be a better way to write the that judgment?
Well for starters I wouldn't have lost sleep over an arrow. (Even ⇒... blasphemy, I know.) Instead of, you know, a 3-way intersection sign making me wonder why I need to look both ways before crossing. Or, you know, they could just use a couple keywords from some actual programming languages from this century or get things going in plain English. Maybe "is" or "instanceof" or whatever. Then if you really, genuinely think your readers need to obsess with your formalism (which they very likely don't unless they have the basics down and are also planning to get a PhD in a proof theory-adjacent topic), you can switch from the 21st century English and math notation into cuneiform and hieroglyphics.
(You can probably tell I didn't enjoy the experience...)
I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the idea of (endo)functor from category theory, but people try to rename it (e.g. "Mappable") to make programmers understand it better. In the same way, you're proposing to rename the turnstile to an arrow symbol.
The article "Why 'Functor' Doesn't Matter" [0] is relevant.
In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1].
For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me.
I never got used to it is the thing. And I spent a heck of a lot of time on it. Yet I still look at a link like [1] and it may as well look like hieroglyphics to me. It's not that I can't parse it, it's just that it's like forcing me to do 500 push-ups in the process, to communicate something that shouldn't need more than 10 push-ups to warm up at most. Mathematical notation isn't all like this. Some stuff is actually intuitive. PL/proof theory notation just seems to be actively designed to make your life harder for some reason.
Well lambda calculus always looked weird and unapproachable to me until I finally sat down one day and said "I'm going to finally learn this" and it was really, really easy after an hour or two of going through the notation. Sometimes math is like that.
I spent way more than an hour or two on this. And even by the end, it wasn't that I couldn't read it, it's that it was always a process of perpetual dragging me through molasses.
Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on).
However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.
In this context, ‘A’ is an instance of Type, and ‘Type’ is the type of types (usually the term used for type of type is Kind). So while ‘x’ could be the value 7 and ‘A’ could be the type Int, the ‘B(x):Type’ means that the value of B(x) is some Type, could be Int, Char, Bool, etc.
The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C).
On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`).
The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".
What is your point exactly? My response, when faced with something like this, is to be excitedly curious, and try to find out what the notation means, maybe by searching "type theory notation" and going a couple of links deep to find at least the start of an explanation – not to publicly throw up my hands on a comment thread. If I was really at a loss I might ask for some pointers to introductions to the topic. The article is clearly written for people at least somewhat familiar with the domain and notation, and a bit of research shows that it's quite standard notation.
Me not so much, while playing around with Idris and the respective book exercises was interesting, we aren't going to be doing GUI RAD tooling with such languages for the foreseeable future.
It might sound silly, but the scene hierarchy and inspector in Unity is actually quite good and very useful for game development. Sometimes I find myself missing having it in other programming systems as well.
When moving from dynamically/untyped/unityped languages to those with types, you are liberated from having to check the shape of inputs. If you're given something that claims to be a list of strings, it absolutely is a list of strings, and you can proceed without thinking about it's list-ness or string-ness any further.
When moving from a typed language to a dependently typed language, you are liberated from having to check the state of inputs. You don't have to worry that your file handle is closed, or ensure that you update the state of the object correctly to satisfy some protocol (if you don't, you will be picked up on it!). If you are writing a parser, you don't need to check that the parser returned the form that you just called - you know upfront.
There are other niceties: the type of the function is always a very rough exposition of what the function should do. With dependent types, it becomes considerably clearer. Consider these two functions, which could have very similar implementations (in some Idris-like syntax):
f : Int -> Int -> Bool
data T : Int -> Int -> Type where
Tz : T 0 x
Ts : T a b -> T (a + 1) (b + 1)
g : (x : Int) -> (y : Int) -> Maybe (T x y)
Given just the structure, it should be a bit clearer as to what's going the functions intend to do.
But wouldn't the actual code tell you exactly what the function does? Why is it beneficial to have a similar version of the same in a more or less different language expressed separately?
The flipside of your description of moving from un typed to typed to dependent typed languages is the amount of specification you need to think about and add to your code. This is awesome for component interfaces, but it can often get in the way of internal code. For example, if I try to redactor a long function and extract a few bits, those bits may only be called with very specific argument values, despite what the types I have on hand (or am willing to define) might say. Languages without some dynamic escape hatches can force you to create code that is too general, or define extremely specific types, for situations that really don't call for it.
It also makes very generic or dynamic code much harder to write, or requiring ever more complex constructions. For example, most mainstream typed languages can't express something as simple as 'a function that returns either an A or a B' without resort g to dynamic typing and casting. And even in Haskell, a lot of code is more loosely typed than might be expected. For example, even though measurement units are often touted as a feature of typed languages, there are no complex mathematics libraries that use measurement units, simply because it is so much effort to correctly type everything, for relatively little gain.
Yes, the actual code will always tell you exactly what it does.
There is always a necessary distinction between specification and implementation: if there weren't, one of them would have no value. We often suggest that the intent of a piece of code should be specified in comments, and this is in that category. This way, the compiler can read your comment and figure out if it needs updating! Languages without dependent types work this way too - but you have to try very hard indeed to be eloquent in type signatures, and being able to talk about values lets you say a bit more.
Coming onto your second point: if the function is only valid for some set of values of the given type, why is it 'not really called for' to create specialised types for it? If you call it with something else and it runs, it will be a bug. Newtypes or wrappers are common patterns.
I think that most mainstream typed languages have common constructs to offer that 'A or a B' value you want: this is solved via inheritance, `Either`, `Result`, or `std::variant`.
Types don't generally specify intent as well as comments do. They still can only tell you what the code does, not really why. They do clarify some assumptions the implementation makes, essentially defining pre- and post-conditions, which you'd normally write in comments if you didn't have types. But at some point, it does get much easier to say 'performs a stable sort' then to define the dependent types to express that the list is sorted and that the order of equal elements doesn't change.
My point about newtypes and wrappers is that they are almost pure overhead for helper functions. There is a reason why we don't define precise types for each of our intermediate calculations in general, and this doesn't change when we move those computations to a separate function.
Finally, inheritance is not a real solution for returning A or B, with inheritance I can only return a C that both A and B derive from, and this C often doesn't exist and can't be added post-hoc. What you normally do is go for Object or void*, which is much closer to dynamic typing than inheritance. And most mainstream typed languages don't have Either or Result. C++ with std::variant is the only exception, I forgot that it was added. BTW, I should be more explicit - the way I see it, the mainstream typed languages are Java, C#, C, C++, and maybe Go.
This is quite wishy-washy but in my experience the magic of type driven development is feeling like you’re working with the computer.
You can achieve this with other languages (e.g. Smalltalk), but many of the most popular languages feel more like inanimate tools (some very good ones!).
I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reasons I love them so much:
- The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It's so satisfying to write code and prove it correct (with a type checker to catch your mistakes), but so few people get to experience this feeling.
- But dependent types are also useful in ordinary everyday programming! Many "features" of programming languages that we use at work are actually just limited special cases of the general idea of dependent types. For example, in a dependently typed language, you don't need special support for generics—you get it for free!
- Dependent types also eliminate much of the need for macros. In Rust, for example, you might use a macro to generate a JSON parser for a given type. If you had dependent types, you could just write a function that takes your type as an argument and returns the parser!
- Of course, there's that famous example of length-indexed vectors. The idea is that you can keep track of the sizes of your arrays in their types, and statically prevent out-of-bounds errors. So, for example, trying to get the first element of an empty array would be a type error.
- Haskell's generalized algebraic datatypes are another example of a limited special case of the full power you'd get from a dependently typed programming language.
- Another example: some languages have special support for existential types in some form or another. For example, Rust has something called "impl Trait" which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism).
- Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution.
Dependent types may seem complicated at first glance. But after seeing how all these programming language features collapse into a single unified framework, you might change your mind: dependent types are extremely simple compared to the cornucopia of concepts we have to learn in their absence! I strongly believe that programming languages have grown too complex, and dependent types have the right power-to-weight ratio to cull that complexity.
The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs.
Hopefully Rust will evolve into it or a new language will come up for that: we really need this to finally have a programming language that is strictly better than all others and can thus be the single language in use and finally the solve the programming language problem.
> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs.
The Coq language groups types into two categories: Set and Prop. Prop, which (informally speaking) contains all your proofs, is erased when you "compile" your Coq code into another language like Haskell or OCaml. This is something people have thought about quite a bit already.
I think the reason people aren't using dependent types has more to do with the ecosystem around these languages: the tooling, the libraries, the documentation, the tutorials, ... None of that is where it needs to be for these languages to be appealing to industry programmers.
> Hopefully Rust will evolve into it or a new language will come up for that: we really need this to finally have a programming language that is strictly better than all others and can thus be the single language in use and finally the solve the programming language problem.
I have serious doubts about this. Rust, like every mainstream language, already has too many features that overlap with what dependent types give you for free. Also, Rust is not a functional language (some people claim it to be, but there are side effects everywhere!), so it would be a bit of an impedance mismatch.
As much as I'd like to believe in this unicorn language that is better than all the others, experience has taught me to be skeptical of that. Programming is used to solve so many different kinds of problems that it's hard to imagine a one-size-fits-all solution, but I won't claim it's impossible.
AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM machine.
Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
The issue is that I think all of the current dependently typed languages don't have zero-cost abstraction and compiled code efficiency as a primary goal, they are designed for research or as machine-checked proof systems.
There's also the issue that some features may not compose well, e.g. Rust's ability to mutate a single field in place (needed for zero-cost since CPUs can do that with a store instruction) doesn't compose very well with dependent types because that can change the type of other fields, and also linear types (again needed to fully use CPUs) don't go well with having proof-like types that refer to other values, etc. All this seems fixable, but it seems quite involved to find the most general and ergonomic solution.
> AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM machine.
You don't need linear types for in-place updates. You can use a monad (which is another thing you can easily do with dependent types) to express the side effect of doing mutations. Then you can compile that monadic Coq code to Haskell, which then compiles to efficient machine code that actually does in-place updates.
Though, perhaps it is also worth mentioning that Idris 2 has both linear types and dependent types.
Regarding the need for automatic memory management: yes, most dependently typed languages have a garbage collector, but many "real" programming languages have garbage collectors and programmers are still happy to use them. I don't know why everyone in this thread is so concerned about performance. Dependently typed code can compile to reasonable machine code without any stretch of the imagination.
> Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
Memory layout is certainly something that needs to be dealt with, but compilers can monomorphize where possible to generate fast code with unboxed types in many cases. I don't think this is the main blocker for dependent types. I've written dependently typed code that easily outperforms the dynamically typed code I write for production at work (by at least an order of magnitude). In fact, dependent types can be used to guarantee that certain things don't need to be checked at runtime, which can in some cases give even better performance than what you'd get in a regular old statically-typed language.
Tangential: How would the function `first :: &(Vec a) -> Option &a` (which, given a non-exclusive reference to a vector, returns a non-exclusive reference to the first item of the vector, with the same lifetime) be typed using linear and / or dependent types?
I'm certain that this can be modelled using dependent types (after all, anything can), but I can't think of a way to do it that's anywhere near as ergonomic as Rust.
Monads work for just doing in-place updates, but they seem unable to also prevent/control mutable aliasing, avoid rc/gc of arrays/records, put arrays/records inline in the containing record, and anyway they unnecessarily linearize code, which also seems to play badly with providing proofs.
Mandatory GC is not a zero-cost abstraction (it is ridiculously inefficient and unnecessary in general), and a language with mandatory GC is a non-starter as a universal language. C programs (like web browsers) are starting to have new code written in a different language only now that Rust is available as the first zero-cost non-GC safe language.
Yes, dependent types improve performance by eliding checks, but that's only likely to be a net win if the rest of the compilation is optimal.
I agree with your point in general, but I think it is vastly exaggerated to call GC 'ridiculously inefficient' or 'unnecessary in general'. For many common problems, GCs add at best constant overhead. And, almost all highly performance critical programs have some kind of (admittedly specialized) GC mechanisms in place, because often releasing objects as they go out of scope is not efficient enough.
Even more, the performance limitations of most GC languages have more to do with the lack of good ways of writing code which simply doesn't allocate, rather then the problem of collection. GCs are often faster than malloc/free, but not as fast as simply not allocating/freeing anything.
Finally, it's important to remember that there are algorithms that are significantly more difficult to implement without a GC tahn with a GC. Even simple compare-and-swap atomic sets can require many times more code and care to implement if you have to handle cleanup of temporaries as well.
All non-toy languages and compilers only add constant overhead; unfortunately that's still a problem, the goal is to not have any overhead at all.
malloc/free is fast with a moving GC, but moving is not, and if an object is never moved it's likely that it should not have been allocated on the heap in the first place.
The cmpxchg problem is solvable by epoch-based reclamation libraries (RCU, crossbeam-epoch, etc.), and while a traditional GC also solves it, it's not necessary.
> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs.
AIUI, dependently-typed languages don't really have a fixed phase distinction between "compile time" and "run time". The type checking pass can involve execution of "run time" code (this is one way to understand why these languages are generally not Turing complete), and "run time" code may be required to somehow build complex code like a JSON parser "on the fly", depending perhaps on user input.
In practice, some systems have a "code extraction" component that's intended to filter out the "irrelevant" parts of the code and transpile it to a conventional programming language, which obviously reintroduces a separate "run time" deployment step. This could definitely be done using, e.g. Rust, provided that the issues due to a lack of general GC in that language are addressed too.
I've been trying to learn enough about this problem to be of use in implementing this (playing around with my own language implementations). It seems like a real challenge might be around ensuring that your programs have extraneous 'type stuff' removed in the compiled program. Part of this could be helped with a nice way of doing proof irrelevance (eg. something like Quantitative Type Theory) and another could be multistage programming (eg. something like MetaML or MetaOCaml). The latter would make it much easier to do a more general form of Rust's monomorphisation of type parameters. You'd then may also want some sort of uniqueness typing and borrowing, but I have no idea where to get started on that! And you also don't want to drown in a mountain of annotations!
> aimed at programmers rather than mathematicians and computer scientists
Do it! There's a dearth of such a format for the more "hi-falutin" topics out there. Doesn't need polish or total precision either, "us programmers" can deal with IRC-like stream-of-tid-bits.
Question: if compile-time evaluation of language X is fully-featured-fully-capable X (sans IO / syscalls, say) with "types as values" (of compile-time-only type `type`, say), ie. given Turing-completeness, where you can have functions that build up and return types --- do you still need complex theoretical type system constructs like "dependent"/"refinement"/"row-polymorphic" etc natively.. say at compile time, given sufficient prim builtins and storage-describing "prim types" (int, arr, tup) any further type-details are described programmatically. I suppose this leads to being able to express predicates that the type checker can "evaluate" in tandem with those compile-time evals..
I haven't gotten to the dependent types part yet. I find most tutorials one these languages start with the theory up front. I'm taking a more pragmatic tack by demonstrating the language through examples building on familiar learning patterns of writing simple programs first and working your way up.
I'm generally interested in this, but (even as somebody who knows intermediate Haskell), I don't have a good intuition about the scope of dependent types:
- how much of the burden of writing the proof falls on me, and how much falls to the compiler? I've seen Idris type signatures, and I didn't find them super easy to grasp.
- What are the full range of things I can express? What can't I express, even with dependent types? I come from math, so I'm used to have infinite flexibility to define what goes into my set of possible values. When I first learned Haskell I was surprised that I couldn't easily define types like "this set, modulo an equivalence relation". Or something like: "Int, but only even numbers".
- how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through? I already run into this all the time in Haskell, with Maybes thay I _know_ to contain a value, or Lists that I know not to be empty. There is a real trade off between writing clear code, and wrapping/unwrapping values all the time everywhere.
Length-indexed vectors is a great example, because it is such a non-story in math, and yet for programming I have to front-load all this complexity to express something so utterly trivial. It's part infuriating, part enlightening how surprisingly tricky seemingly small things can be.
> - how much of the burden of writing the proof falls on me, and how much falls to the compiler?
The compiler in Idris can do some magic, but usually the burden is mostly on you to write proofs. Idris (and similar languages) have assistance in editors to help you automatically write code and proofs.
> What are the full range of things I can express?
Dependent types as present in Idris, Coq, Agda, etc. can serve as a foundation for mathematics, so… pretty much anything!
For your example, most such languages don't have quotient types, so you'll still need to use setoids or similar to model quotients.
> - how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through?
It's pretty much the same situation as Haskell or Rust, but I think having to write fromJust / unwrap is great. It tells you when you're reading the code exactly what assumption has been made, and it doesn't seem awfully burdensome.
> yet for programming I have to front-load all this complexity to express something so utterly trivial.
What's "all this complexity" that you're referring to?
I, for one, would be quite fascinated by such a blog post - you make it sound downright magical! I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing?
Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
Maybe with shelter-in-place I'll have time to write it. :)
> I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing?
Most of my experience with dependent types comes from a language called Coq (as well as one of my side projects, which is a new dependently typed language). Agda and Idris (among others) also support this style of programming. Idris goes further and uses dependent types to provide amazing IDE capabilities. There's a YouTube video where the designer of Idris used his IDE to automatically implement matrix transposition (the type was so precise that the compiler discovered the only sensible implementation).
Unfortunately I think the world is still lacking a good general-purpose dependently typed programming language suitable for production use (though I'm working on it).
> Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
Generally speaking, dependently typed languages are functional. The fundamental concept in dependently typed languages is the dependent function type, also called "pi type" or (confusingly) "dependent product type". So, the whole thing is based on functions and their types. One could imagine some kind of hybrid language, but combining dependent types and implicit side effects (like imperative languages have) is an active area of research.
Damn, this area of programming sounds very interesting, but I'm so so lost in these type compositions... Is it this Idris video you are talking about? https://youtu.be/X36ye-1x_HQ?t=1716
I'm already having troubles following it after 8 lines of type definitions, while matrix transposition in the language of my choice is just `#(apply mapv vector %)`
Sorry, I'm not trying to be dismissive, I just want the ergonomics of expressing my intentions to the computer be free of all this boilerplate while leaving compiler a possibility to give me some useful feedback when something might be wrong, are we really not there yet or are there languages aiming to make dependent types practical? You mentioned Coq, but I'm still not being able to find any code examples or some getting started guide in its official documentation...
Do dependent types really eliminate the need for macros? As far as I can tell you cannot pattern match against values of type Type in dependent languages, so I don’t see how you could generate a JSON parser without some kind of reflection.
I sort of glossed over the differences between macros and dependent types in another answer in this thread, but I'll expand on it here. Typically the term macros is used to imply one of two things (that may be used in the same instance of a macro):
1 - 'compile-time' code execution of some arbitrary code with the result of that execution then being available at run time
2 - a specific type of function which takes the AST of some language and then uses some procedural methodology to mutate/alter that AST transforming it into some other AST
I would say, that while dependent types can be a useful basis for covering several of the typical use cases of macros, they do not without some additional structure, provide a firm proof/type theory for the whole scope of macros.
I would suggest that the most sound attempts at describing the computational phenomena encapsulated by the most common usage of the term 'macro' would be found in the following:
a) implementation of Temporal Logic (per Frank Pfenning's interpretation) for description of compile-time code execution and
b) implementation of Modal Logic, describing multi-staged compilation, as in Davies and Pfenning
So, I would not say that dependent types can eliminate macros, but they do cover a chunk of the areas that are often implemented by macros, including generics and other type based compile time code patterns.
How is that a function working on types not a macros, if that function is executed as part of the compilation process? And how is that function efficient if it is not executed as part of the compilation?
It is a stretched analogy and omits both practical (at the proof level) and theoretical subtlety, but you can sort of think of a dependently typed function as a compile time macro or a template-like generic. However, I think it would be fair to say that macros and generics are merely a mechanized implementation of a very small slice of what dependent types are capable of in full generality
If you want to read a somewhat longer treatise about dependent types and language, try the book "Modal Homotopy Type Theory". Modal logic has been basically invented for linguistic problems.
I don't think dependent types are essential for giving language a formal semantics though, I think discourse representation theory has a more direct approach.
> The main characteristic of the language of mathematics is perhaps that different members of the community can completely agree about the meaning of each word and sentence.
Haha, this got a laugh out of me :). While this is true in principle, the reality can be quite messy! For instance, there seems to be little consensus about what the words "vector", "contravariant", "covariant", and "coordinate" should mean on the Wikipedia page [1] claiming to explain just that!
No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system; which has great implications for type safety and so on.
A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }".
My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.
The example normally given is, for instance, being able to define a function whose return type depends of the value (not the type) of its argument – for example, a function which takes in a natural number and returns an array with exactly the length of that natural number.
Dependent types are one of the axes in the Lambda Cube: https://en.wikipedia.org/wiki/Lambda_cube – types have terms the way sets have elements (roughly speaking) and so you can [1] relate types with types (type operators), you can [2] relate terms with types (polymorphism), and lastly [3] types with terms (dependent types) – giving a three-dimensional type theoretic space.
(Btw, I don't know if it even makes sense to talk about relating terms with terms or what feature of type theory captures this notion – so don't ask me!)
Okay...
> x:A ⊢ B(x): Type
I'm lost.