Julia has no dependent types

[nox]

Even though the manual says so, that is pure namedropping.

[vtjnash]

https://groups.google.com/d/msg/julia-users/lgeq0xzjf9I/vzFfFbqZDmcJ

possible dup of #6081

[nox]

By this definition, Erlang is dependently-typed because its tuples behave like Coq vectors and Smalltalk is dependently-typed because you could make class objects that depend on arbitrary values. Buzzword.

[Keno]

What definition of dependent types would you like to use?

[nox]

The one everyone agrees about, that you can't have them in a unityped language.

I can do foo({matrix,Dimensions,_}=L, {matrix,Dimensions,_}=R) -> do_something(L, R) in Erlang and that doesn't make Erlang dependently-typed; just like claiming homoiconicity was wrong, saying that the language is dependently-typed is wrong too. You don't even explain in the documentation how it has dependent types, the term is just dropped in a list of qualificatives.

[jonsterling]

Try finding one actual Type Theorist who wouldn't cringe on hearing the claim that Julia is “dependently typed”...

To grasp what it means to be “typed”, please read PFPL. To understand the definition of “dependently typed”, any one of the myriad beginner-level papers and expositions will do. Then, perhaps you will reopen this issue with a changed opinion.

[jonsterling]

(By the way, if you don't own PFPL yet, which seems likely, give me your address and I will literally buy you a copy and send it to you. This is a real offer from someone who wants to actually help you.)

[cartazio]

I apologize to all for the tone this thread has taken. The core premise "don't coopt widely used technical terms to mean things that they dont mean". Kinda like the word Literally :)

However, a better name for the idioms julia takes would be "strongly runtime checked/typed, dynamic dispatch over types". (ignoring the dimension of here "types" meaning "runtime data type tags/information").

Dependent types means a very very specific thing (roughly): that the Static semantics of the language corresponds to some (subset) of formulae in a higher order predicate logic, with the program terms being the "proofs" of those formulae. The "static semantics" is also known as "type checking before you run the program". Examples of dependently typed language include Coq, Agda, and Idris.

A key detail with these and other dependently typed languages is that theres some sort of "logical specification" that you can validate before the program is run! Likewise, a crucial feature in a "dependently typed" language is "inductive type families", which is a pretty deep topic on its own. Heres a section about the topic in the coq manual. Theres also a bajillion more papers on this stuff, heres a cool one I've not seen before (a deep rich topic thats still an active area of research).

I'd love to see Julia have dependent types (it sadly lacks them!), they are a wonderful tool for mathematical modelling, verifying the correctness of algorithms / computations, and they interact wonderfully with expressing the invariants that matter in numerical algorithms especially! (I'd know, I've been spending the past 2 years basically writing dependently typed array libraries in an industrial setting.).

I do think adding dependent types would be a boon to Julia, but theres a lot of great tools that would be easier to adapt to julia, Contracts are one! They're a great tool in Racket Lang, (Racket being Scheme variant that I think Julia draws many ideas from in spirit / practice).

Contracts are kinda the Dynamic language version of dependent types and theres been a lot of work by many, smart, programming language researchers to make them great. I believe theres even some work that shows that contracts help with making a tracing jit even awesomer, though I can't recall off hand any good starting points for that.

There are ways that contracts can "evolve" into being a "dynamic" form of dependent types, but thats beyond the scope of this thread. Currently however, when a julia-ist says "dependent types" they actually mean "we can case analyze at runtime over the input types, and depending on that, return different result types", a la multimethods.

I humbly ask that Julia consider respecting the meaning of words in the technical domain of programming languages research, as Im sure they strive to do in the numerical computing domain.

Thank you for your time and consideration.

PS: I'd rather not, but If need be I can (will) pester various junior faculty i'm friends with to pop on this thread and agree with me. But I really really dislike argument from authority, they make people defensive and they inhibit learning.

many thanks
-Carter

[StefanKarpinski]

The one everyone agrees about, that you can't have them in a unityped language.

Julia isn't a unityped language. Calling dynamic languages "unityped" reveals an unfortunately common but fundamentally nonsensical point of view: that a "type" must be something that you check at compile time. Not, mind you, that you can check it at compile time – but that you do check it at compile time. It doesn't take much thought to understand why it's problematic to define what something is by how you use it. Does a chair stop being a chair if you bolt it to a wall in a gallery instead of sitting on it? You can run the Glasgow Haskell Compiler (GHC) in a mode where it defers all type checks until run time. If you run a type-correct Haskell program this way, do Haskell's types suddenly cease to be types? Has the meaning of the program changed even though its code and behavior are both identical? Does the existince of this GHC mode make Haskell a unityped language? Clearly that's nonsense. A type is a type, regardless of when you check it. These days you can type check a fair amount of Julia code at compile time. Does that suddenly make Julia's types "real types"? If you're going to claim that dynamic languages don't deserve to use terms like "types" and "dependent" – even though Julia's type system is much more sophisticated than the vast majority of statically checked languages and having the dimension of an array as part of its type is the classic example of dependent typing – I'm afraid you're going to have to come up with a more coherent argument for why Julia doesn't have "real types".

[cartazio]

@StefanKarpinski can we shift this to IRC for span? feel like this is better as a dialogue than chain of chain letters

[Keno]

I apologize if my comment came across as aggressive, it was not meant that way (early in the morning comments ;)). I will readily admit that my knowledge of formal PL theory is limited, which is why I asked what the common definition is (I was rather set back by the confrontational tone of the original issue and the subsequent comments). Thank you at @cartazio for your well worded comment - much appreciated. As a rather theoretically oriented person, I appreciate the value of theory in guiding implementation, but I fear that it may box you into categories that turn out not to matter all that much in praxis. I am genuinely interested in the correct definition here and will read up more on the topic (and ask around in the CS department) to form my own opinion, but I will refrain from making any further public arguments in either direction as there are other people that are more qualified than me to make such arguments (and I don't think I'd be able to convince anybody anyway) and I do not think it's the best use of my time.

[cartazio]

@loladiro good theory can help unbox you in, bad theory is the culprit on the rest.
feel free to holler at me on #numerical-haskell if you wanna here my take on how theory can help numerical computing

thank you @StefanKarpinski and other folks for being responsive on this ticket.
Also paragraphing is handy sometimes ;)

[nox]

Calling dynamic languages "unityped" reveals an unfortunately common but fundamentally nonsensical point of view: that a "type" must be something that you check at compile time. Not, mind you, that you can check it at compile time – but that you do check it at compile time. It doesn't take much thought to understand why it's problematic to define what something is by how you use it.

What I meant by unityped is clearly explained by Robert Harper.

You can run the Glasgow Haskell Compiler (GHC) in a mode where it defers all type checks until run time. If you run a type-correct Haskell program this way, do Haskell's types suddenly cease to be types? Has the meaning of the program changed even though its code and behavior are both identical? Does the existince of this GHC mode make Haskell a unityped language?

Given that all type checks are deferred to runtime, it makes all expressions inhabitants of all types, making Haskell in that mode unityped.

Clearly that's nonsense. A type is a type, regardless of when you check it. These days you can type check a fair amount of Julia code at compile time. Does that suddenly make Julia's types "real types"? If you're going to claim that dynamic languages don't deserve to use terms like "types" and "dependent" – even though Julia's type system is much more sophisticated than the vast majority of statically checked languages and having the dimension of an array as part of its type is the classic example of dependent typing – I'm afraid you're going to have to come up with a more coherent argument for why Julia doesn't have "real types".

I will just ignore that part given that I never argued that dynamic languages don't have types at all. Just that expressions at compile-time are all inhabitants of a single big union type. That the values themselves are tagged with a type is a completely different matter. And that some contracts are statically checked at compile-time is also a different matter.

[puffnfresh]

@StefanKarpinski thanks for updating the docs!

[StefanKarpinski]

Ah yes, that Robert Harper post is a perfect example of the view point I'm talking about. Laurence Tratt has already rebutted it rather eloquently, so I'm not going to repeat what he's already said.

[puffnfresh]

@StefanKarpinski from the article:

Bob points out that, conceptually, a dynamically typed program has a single static sum type ranging over all the other types in the program. We could therefore take a dynamically typed program and perform a conversion to a statically typed equivalent. Although Bob doesn't make it explicit how to do this, we can work out a simple manual method (though it's not clear to me that this would be fully automatable for most real programs). We would first need to see all the points where the program performs operations that use types (perhaps by a sort of type inference; but we'd also need to include dynamic type checks using e.g. isinstance in Python or instanceof in Java). All the types referenced would then be ranged over a single sum type. Whenever a sum type is encountered statically, we would then need to use a typecase to check the dynamic type of the value, and then perform an appropriate action. In this way we can guarantee that our once-dynamically typed program is statically type-safe.

This conceptual argument is quite correct.

The rest of the article is trying to describe the implications of the above, absolutely not rejecting the premise.

[StefanKarpinski]

Given that all type checks are deferred to runtime, it makes all expressions inhabitants of all types, making Haskell in that mode unityped.

In that case being "unityped" or "multityped" is a property of the implementation rather than the language itself.

I will just ignore that part given that I never argued that dynamic languages don't have types at all. Just that expressions at compile-time are all inhabitants of a single big union type. That the values themselves are tagged with a type is a completely different matter.

As it happens, the Julia compilation process assigns much more specific types to most expressions at compile time – this is how we generate fast code. The majority of expressions have completely concrete type inferred at compile time – although obviously that figure depends on the program in question. All of this is an implementation detail, but you've already stated that "unityped" is a property of an implementation (e.g. GHC in dynamic mode) rather than a language (e.g. Haskell). In this case you're still wrong since Julia's implementation happens to assign fairly specific types to expressions. A large amount of the time its values are not tagged or even heap allocated.

But of course, this premise that whether a language is "unityped" or "multityped" is a property of the implementation is crazy. Haskell is still Haskell when you run it in dynamic mode – the semantics of the language don't change based on whether you do type checking or not.

[pozorvlak]

However, a better name for the idioms julia takes would be "strongly runtime checked/typed, dynamic dispatch over types".

I think that the use of "dependent" in the docs was really to indicate that types (in the sense used by the dynamic language community) can be parametrized by values - see eg Julia's Array type which is parametrized by both the type of its elements and its rank (an integer). This feature is highly unusual, and it would be nice to have a word for it :-)

[cartazio]

well said @pozorvlak.

[jonsterling]

Dependently tagged?

[mschauer]

They are called "parametric types" at various places in the documentation, what is wrong with that?

[jonsterling]

The problem is specifically that they are not types, and very likely not even parametric.
JMS

On Mar 11, 2014, at 11:27 AM, M. Schauer notifications@github.com wrote:

They are called "parametric types" at various places in the documentation, what is wrong with that?

—
Reply to this email directly or view it on GitHub.

[JeffBezanson]

Something can hardly be opposed to that of which it is but a trivial special case.

Sure it can. You oppose anything outside the special case. Examples abound. Monotheism?

[cartazio]

parametricity is a wonderful topic, some good reading on it might be http://lucacardelli.name/Papers/SRC-109.pdf (the abstract and first page alone give you a lot).

"Parametricity" as a formal property is kinda like saying "given just the type, because we know the code is oblivious to what the specific types supplied, we know the definition must be of the form X"
eg a function of type

(a->b)->a -> b

must be function application (or an infinite loop)

Not every "generic" function thats useful has this "strong parametricity" , and in Rust and Haskell, this is handled with Traits/TypeClasses. You don't get the same parametricy here, but you can still get something close

renderToString::(Show a)=> a ->String

we know renderToString will somehow turn a into a String, then do something with it, and return the resulting string.

by making it clear "when/which" type cases will happen in the code syntactically, you can actually have stronger promises in how it will work

aside: also, can everyone act like the adults they allege to be? I'm getting embarrassed by both sides. Either everyone be respectful and adult like, or I will get some damn popcorn and stop helping

[JeffBezanson]

Some of the terms here have both formal and informal senses. For example python has a function type to get the "type" of something, and I don't think it's worth arguing with them that they're misusing the word "type". Everybody knows what they mean by it.

I know there are contexts where one is supposed to call these things "tags", but I don't find it very helpful to do a global search-and-replace of "type" to "tag". I will also echo comments above that just because types aren't statically checked doesn't mean they aren't there. For every tag and every term, there is a proposition that the term will yield a value with that tag. Ok, these propositions are generally undecidable, but that is a different issue. Informally, one will sometimes move between the tags and the propositions without being too careful about it. But in dynamic languages the latter are not much used or discussed, which is why those communities freely equate "type" and "tag". A common phenomenon with terminology of any kind.

[StefanKarpinski]

I fundamentally reject the notion that a small subset of PLT people can unilaterally lay claim to terms like "type" and insist that they cannot be used except when they deem it worthy. The term "dependent" I care less about, although it's pretty obnoxious to insist that this term, which has an obvious meaning in this context, and for which there is no other term, should not be used, because, you know, you said so. There are obviously a lot of interesting systems that are not statically decidable – and the majority of code in the world these days is being built in such systems. Julia's parametric types are the natural fully dynamic analogue of parametric types in your favorite static language and types like Array{T,n} are the natural dynamic analogue of dependent types in such systems. Insisting that we not use the obvious terms does not really help make talking about any of this clearer.

[puffnfresh]

@StefanKarpinski why do you think it's a small subset? What's the definition of type outside of this subset?

[StefanKarpinski]

Look no further than Wikipedia: https://en.wikipedia.org/wiki/Data_type.

[puffnfresh]

@StefanKarpinski I meant outside but still within PLT, or does that Wikipedia link still stand?

[StefanKarpinski]

I'm talking about PLT people who study static type systems and insist that something isn't a type unless it happens to be statically checked as a miniscule subset of all the people who use and talk about programming languages. There are, of course, people who do PL research and don't have quite such a narrow-minded view (such as Laurence Tratt), but there is a "no true scotsman" effect in play – you probably won't consider anyone who doesn't agree with you about what a type is a real programming language person, and @jonsterling will offer to mail them a copy of PFPL so that they can learn about real programming language stuff from Robert Harper. This impressively condescending twitter thread is a perfect example of this in action. Excerpts:

@jonsterling Or if they want to be educated by fire, @existentialtype. We could just mail a copy of PFPL.

@cartazio: I've tried to engage with them. But they're like "we have pl experts" (they mean grad student)

I'm guessing that's a reference to @JeffBezanson? I'm not sure. None of us has ever said we had "PL experts" so I'm not sure where that's coming from. In any case, Robert Harper, brilliant and accomplished though he is, still is just one man and neither he nor anyone else gets to dictate what terms like "type" mean. The vast majority of people who use programming languages know exactly what we're talking about when we talk about the "types" of values in Julia but would have no idea what we were talking about if we talked about "tags". When you're insisting on terminology that the vast majority of people who you might want to communicate with wouldn't understand, you might want to reconsider your terminology. Of course, if you only want to communicate with other PLT people who already agree with you, then carry on.

[cartazio]

lets just all shelve this for a while and chat again when we're all in cooler frames of mind. this isn't constructive, and everyone is alienating everyone. which is dumb

[JeffBezanson]

I believe my previous comment explains my position in a perfectly rational fashion that does not alienate anybody.

[StefanKarpinski]

[jonsterling]

@StefanKarpinski That is awesome.

[catawbasam]

Maybe those folks who wish to continue this discussion could take it a more appropriate forum. Lambda the Ultimate comes to mind.

[ekmett]

Haskell is still Haskell when you run it in dynamic mode – the semantics of the language don't change based on whether you do type checking or not.

This is actually not true.

Due to typeclass resolution taking place at compile time, the semantics of Haskell are defined à la Church, not à la Curry. The types do affect the semantics of the resulting expression. Operationally this takes place by type inference causing the correct dictionaries to be passed in based on the result of type inference. This is why a Haskell program can have functions that are overloaded on their return type.

This isn't something that is possible in an calculus à la Curry, or a purely dynamically typed language.

Even as a strongly-typed PLT weenie, I don't try to lay claim to the term 'type'. I work with enough lispers and schemers and R developers and have done enough work in those settings to not have that bias. But that said, saying you have dependent types is a very specific claim that just doesn't make sense in the dynamically typed setting and saying that you support them when you don't support the kind of static checking that they imply comes across as misleading at best and disingenuous at worst.

[tknopp]

Its kind of sad that people get so angry just because of some words on the homepage. A friendly reminder that the term dependent types can be misleading would have been more helpful. I can just applaud Stefan and Jeff for keeping calm and discussing the issue in a constructive manner.

[BekaValentine]

@JeffBezanson what is monotheism opposed to in this case? polytheism/atheism/pantheism/etc? sure, but monotheism is not a special case of those. it's a special case of theism, which it isn't opposed to.

[tel]

I think there's a larger argument which is at a standoff, but a smaller argument around the more specific term "dependent type" which is still interesting. I believe that it's misleading—not from a PLT weenie desire to be right kind of way, but instead because of this

https://www.google.com/search?q=%22dependently+typed%22

If you interpret "dependently type" as a phrase where we're talking about the word "type" (with its contested meaning) being modified by "dependently" then we probably can't make any headway in this discussion.

But if you treat "dependently typed" as a technical term then it's clear that it refers to a very particular style of type system embodied by languages like Coq, Agda, Idris, Epigram, Isabelle, Twelf, LambdaPi, etc. It's clear that some of the primary advantages of languages like these is that they can be used as proof assistants.

I don't think there's a claim laid that Julia attempts to fit into the same lineage as that set of languages. Nor do I believe there's a claim that Julia's type system can statically express interesting mathematical theorems and has the property that instantiating those types constitutes as proof.

I also don't believe that "dependently typed" is used as a technical term in any other context.

---

Given all that above, I believe that the smaller argument still holds some water: the current Julia documentation is misleading in its use of the technical term "dependently typed". A reader encountering it for the first time and googling that term will be lead into a lot of literature which will in all likelihood only serve to mislead.

I think the suggestion of using a new technical term which provides the semantic space for Julia's docs to describe the form of typing embodied by the Array{T,n} example is a good one. I also think rewording the documentation to make it clear that the phrase should not be taken as a technical term would be a meaningful fix as well; however, it's a bit more challenging since in dependently typed literature "dependent" is used as a (weaker) technical term all on its own. Still, I think that semantic split could be handled much more easily.

[tel]

As a meta note, the goal for doing this, I feel, is emphatically not to prove or disprove the righteous definition of some set of technical terms. I think there's a meaningful technical discussion to be had about the exact mechanics of typing in various families of languages—but I think arguing over definitions is easy, technically valueless, and, frankly, a little lazy.

So instead, to me, the goal is to avoid definitional wars. There's a lot of good that can come from cross pollination of ideas and it's hampered if everyone lays claim to the same semantic space and has to duke it out over these issues each time they want to talk. Respecting the technical terms of another field helps to make interoperability easier since you don't need as big of a translation layer.

It also, vitally, helps with search. Since, fundamentally, the goal of documentation is to help someone fresh to the topic get up to speed then I think docs should be designed respecting the weaknesses of purely lexical search, a la Google.

Since another purpose of documentation is marketing value and using an already common technical term boosts your Googleability, this does harm Julia's marketing value somewhat. I believe that a lot of the tension here comes from a value difference between people who feel that such a use of documentation is immoral and those who find it beneficial. I also believe that this makes part of the issue a land grab issue and thus tensions on both sides are understandable.

Ultimately, I don't wish to take a side on this last one, but feel that if I'm correct in that supposition that it'll be beneficial in further discussion to be open about whether you're discussing the technical argument, the getting-newbies-up-to-speed argument, or the turf war argument.

[ihnorton]

"dependent" has been removed from the documentation.

[tel]

Sorry about that then. I was operating on outdated information.

[pozorvlak]

@tel: 👍

[johnmyleswhite]

This issue is very old and no longer requires discussion given that the wording that was under debate has been completely removed from the documentation. As such, I've locked the conversation. There was a comment made earlier today on this thread that violated our community standards, but that comment seems to have been deleted.

[nalimilan]

For somebody who's got no clue about what dependent types are, the heat generated by this topic is fascinating. Let's keep it in the archives for posterity -- in 20 years from now people will say "these were the heroic times when Julia started". :-)