My takeaway is that more than I realized the word “type” seems to be synonym for “magic” in a lot of heads.
My expected takeaway was something about sheaf theory but okay seems like that kind of article will eventually arrive and this is more about telling us that fact.
The post is fine, just one “about” higher than I anticipated (so about the plan to make something “about” the title).
My guess when I saw set-theoretic types for a language where every function runs in its own thread was that it would be about sheafs (~set valued functors) but sorry I can’t really elaborate because I never had a chance to go that far (although I would like to), my academic life ended broke on the street and now I am an ignored madman hoping against hope that people can be persuaded to change their priorities without a bloody catastrophe.
I don’t think every function does run in it’s own thread.. (since it’s a pure language I guess in principle it could).
Academia is a strange distorted universe.
people can be persuaded to change their priorities without a bloody catastrophe.
Oh dear, some mighty catastrophes are clearly incoming… the recent record on “people changing their priorities” is not good.
Sigh. I always argue with myself for a pragmatic multiparadigm close to metal language like D, or mathematically correct like Haskell… but feel if I wanted to go that way I’d want Agda, or comfy old Ruby, or cleaner Elixir….
But I think Valim and Matz are on the right track, much about types can be deduced from the code itself.
Hah! The guy is pretty much the same era as me, I (mentally) put my hand up for all his “do you know what / have you used …” questions…
And yes, it frustrates the hell out of me that we have gone backwards on so many fronts.
Alas, I believe the ludicrous situation we’re in is a symptom of how the economy is designed.
eg. I used an excellent smalltalk system in the 1990’s that had a lot of what he is walking about…. it (and a bunch of other excellent products) were bought out…. and left to whither and die.
Parable of the Software Industry: The software industry is like when a miner, through incredible luck, found diamonds lying loose on the ground. He picked them up with just his hands and became the richest miner in the area, hiring hundreds of men to dig for diamonds with just their bare hands. So all the other miners threw away their picks and shovels and used their bare hands… Because that’s what the most successful people were doing.
I think the place to do static analysis is the version control system… and as soon as you do risk assessments then you have premise for “block rewards” (or you know whatever, I’m saying you can have finality with X% risk)..
I would enjoy more detail but I think they are really in a preliminar phase I guess.
From set theoretic types I think they mean intersection and union types.
I have an hypothesis about how an effect system would be like.
I think the dynamic calls (apply/3) can be a challenge, because the type of the message must match a type of the actor, so we would need type PIDs. Since there are process registries, they would need to carry some information about type.
“static types” is kind of short for predictable, well behaved static analysis that work on the whole language (or most of it, when you bolt it in after the fact). I don’t really think it’s “magic” :). I think the talk makes a good job of listing reasons the Elixir team wants them, namely tooling (like typescript), documentation, to allow designing type-first for those who like it, and as proofs in the restricted language afforded by whatever type system they eventually pick.
I’m not following why you jump to sheaves from “set theoretic types” though. Clearly the simplest interpretation of that, is that types are seen as sets of Elixir values, and there would be intersection and union operators on types to handle the fact that Elixir allows to define multiple overloads of a function, and restrictions on a given clause. I don’t know much about sheaves but they seem to be a category theoretic abstraction of set-like things, which doesn’t bring much to the table when talking about a concrete use of sets.
Set-theoretic types are exciting for languages with dynamically-typed runtimes. Cduce and Ballerina are the two languages I know of that have really embraced them. Castagna is definitely a huge influence to set-theoretic types. Covariance and Controvariance: a fresh look at an old issue by Castagna is a great introduction to set-theoretic types (sections 4 and 5 hold the core of the set-theoretic foundations)
Gleam has a very different approach (and a different type system) influenced by ML languages like OCaml, so I don’t see why the two can’t coexist. Being designed with types from the beginning is very different to gradual typing, too, so I imagine they’ll still have different patterns and feel different to use. I’m still keen for Gleam!
Best of luck, I think this is going to be a very difficult endeavor. As TS proved, bolting on a type system to an existing dynamically typed language is definitely possible, but at the expense of type system soundness.
This brings me to the big announcement from ElixirConf EU 2022: we have an on-going PhD scholarship to research and develop a type system for Elixir based on set-theoretic types.
Where does this leave the (seemingly active) Gradualizer project? Would it supercede it? Integrate it?
It reminds me a little bit of the challenges facing Scala: When you’re running on someone else’s VM, with its own concept of what a type is, you’re constantly fighting the assumptions (and lack of assumptions) of that VM.
And I guess it’s probably even harder for Scala, because the VM keeps evolving at a relatively rapid pace, and quite often adopting similar-yet-incompatible changes inspired by the Scala work.
My takeaway is that more than I realized the word “type” seems to be synonym for “magic” in a lot of heads.
My expected takeaway was something about sheaf theory but okay seems like that kind of article will eventually arrive and this is more about telling us that fact.
Valim’s post seems pretty straightforward and sensible to me.
I think you have some context in your mind that is not in mine… because your response makes no sense to me, probably because I’m missing that context.
Could you elaborate?
The post is fine, just one “about” higher than I anticipated (so about the plan to make something “about” the title).
My guess when I saw set-theoretic types for a language where every function runs in its own thread was that it would be about sheafs (~set valued functors) but sorry I can’t really elaborate because I never had a chance to go that far (although I would like to), my academic life ended broke on the street and now I am an ignored madman hoping against hope that people can be persuaded to change their priorities without a bloody catastrophe.
Here’s some justification for my guess (i.e. the context you may be missing): https://www.researchgate.net/publication/222422736_Sheaves_Objects_and_Distributed_Systems
I don’t think every function does run in it’s own thread.. (since it’s a pure language I guess in principle it could).
Academia is a strange distorted universe.
Oh dear, some mighty catastrophes are clearly incoming… the recent record on “people changing their priorities” is not good.
Sigh. I always argue with myself for a pragmatic multiparadigm close to metal language like D, or mathematically correct like Haskell… but feel if I wanted to go that way I’d want Agda, or comfy old Ruby, or cleaner Elixir….
But I think Valim and Matz are on the right track, much about types can be deduced from the code itself.
I think all languages have something to offer which is why I slowly got dragged into thinking about the tooling side and interop.
W.r.t. what we want from the runtime then this guy gets it: https://youtu.be/8Ab3ArE8W3s
I got around to watching that…
Hah! The guy is pretty much the same era as me, I (mentally) put my hand up for all his “do you know what / have you used …” questions…
And yes, it frustrates the hell out of me that we have gone backwards on so many fronts.
Alas, I believe the ludicrous situation we’re in is a symptom of how the economy is designed.
eg. I used an excellent smalltalk system in the 1990’s that had a lot of what he is walking about…. it (and a bunch of other excellent products) were bought out…. and left to whither and die.
Parable of the Software Industry: The software industry is like when a miner, through incredible luck, found diamonds lying loose on the ground. He picked them up with just his hands and became the richest miner in the area, hiring hundreds of men to dig for diamonds with just their bare hands. So all the other miners threw away their picks and shovels and used their bare hands… Because that’s what the most successful people were doing.
I think the place to do static analysis is the version control system… and as soon as you do risk assessments then you have premise for “block rewards” (or you know whatever, I’m saying you can have finality with X% risk)..
I would enjoy more detail but I think they are really in a preliminar phase I guess.
From set theoretic types I think they mean intersection and union types.
I have an hypothesis about how an effect system would be like.
I think the dynamic calls (apply/3) can be a challenge, because the type of the message must match a type of the actor, so we would need type PIDs. Since there are process registries, they would need to carry some information about type.
“static types” is kind of short for predictable, well behaved static analysis that work on the whole language (or most of it, when you bolt it in after the fact). I don’t really think it’s “magic” :). I think the talk makes a good job of listing reasons the Elixir team wants them, namely tooling (like typescript), documentation, to allow designing type-first for those who like it, and as proofs in the restricted language afforded by whatever type system they eventually pick.
I’m not following why you jump to sheaves from “set theoretic types” though. Clearly the simplest interpretation of that, is that types are seen as sets of Elixir values, and there would be intersection and union operators on types to handle the fact that Elixir allows to define multiple overloads of a function, and restrictions on a given clause. I don’t know much about sheaves but they seem to be a category theoretic abstraction of set-like things, which doesn’t bring much to the table when talking about a concrete use of sets.
It wasn’t just because they said “set-theory” it was because it is elixir and they talked about set-theory, but anyway sure, sorry for being rude.
Set-theoretic types are exciting for languages with dynamically-typed runtimes. Cduce and Ballerina are the two languages I know of that have really embraced them. Castagna is definitely a huge influence to set-theoretic types. Covariance and Controvariance: a fresh look at an old issue by Castagna is a great introduction to set-theoretic types (sections 4 and 5 hold the core of the set-theoretic foundations)
How do y’all think this will be in Elixir versus what Gleam is doing? I’m not very familiar with Gleam, but I did read some FAQ: https://gleam.run/frequently-asked-questions/#how-does-gleam-compare-to-elixir
Gleam has a very different approach (and a different type system) influenced by ML languages like OCaml, so I don’t see why the two can’t coexist. Being designed with types from the beginning is very different to gradual typing, too, so I imagine they’ll still have different patterns and feel different to use. I’m still keen for Gleam!
Best of luck, I think this is going to be a very difficult endeavor. As TS proved, bolting on a type system to an existing dynamically typed language is definitely possible, but at the expense of type system soundness.
Where does this leave the (seemingly active) Gradualizer project? Would it supercede it? Integrate it?
It reminds me a little bit of the challenges facing Scala: When you’re running on someone else’s VM, with its own concept of what a type is, you’re constantly fighting the assumptions (and lack of assumptions) of that VM.
And I guess it’s probably even harder for Scala, because the VM keeps evolving at a relatively rapid pace, and quite often adopting similar-yet-incompatible changes inspired by the Scala work.
Nice to see progress! Good luck.