Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ada's dependent types, and its types as a whole

nytpu.com

Post reply on HN
Print view View original

111–120 of 146 posts

Re: Ada's dependent types, and its types as a whole

#111

Post by docandrew »

rad_gruchalski wrote: post #108
seabird wrote: post #6

Ada is a criminally underrated tool that is unfortunately probably doomed to perpetually take the backseat to Rust despite Rust not solving all the problems Ada does. It's really sad that so many people's idea of safe programming is pretty strictly limited to memory safety, and that because Ada's baseline memory safety (SPARK is a different story) isn't as robust as Rust's borrow checker (in the sense that it doesn't…

I really wanted to use Ada, at least learn it. Concepts are nice but I gave up when started looking into unicode support. It was wild, a bit discouraging. Or has the situation changed? What’s the unicode status in Ada?

You can embed and work with UTF-8 strings with no issue (I have source with emoji string literals), but if you need complex manipulation of code points vs glyphs etc. I’m not sure how robust the libraries are for what you are trying to do.

https://ada-lang.io/docs/learn/how-tos/gnat_and_utf_8/

Re: Ada's dependent types, and its types as a whole

#112

Post by cenamus »

seabird wrote: post #6

Ada is a criminally underrated tool that is unfortunately probably doomed to perpetually take the backseat to Rust despite Rust not solving all the problems Ada does. It's really sad that so many people's idea of safe programming is pretty strictly limited to memory safety, and that because Ada's baseline memory safety (SPARK is a different story) isn't as robust as Rust's borrow checker (in the sense that it doesn't…

> We control things that spin real fast and our previous experiences with C definitely resulted in some screwups that left you weak in the knees for a bit.

Ha, you could almost read this as a stuxnet joke

Re: Ada's dependent types, and its types as a whole

#113

Post by pjerem »

throwup238 wrote: post #98
pjerem wrote: post #55

Earlier quoted context omitted.

Let me say that I do agree with you. However I’d add that this job could easily be done by the IDE. For a reason that I fail to grasp, after being around for multiple decades, IDEs are still incredibly bad at presenting useful information on the code. Apart from coloration and more recently type hints, there never have been any real innovation in just helping reading code structure. For some reason we are still stuck…

It’s called “sticky scroll” in VSCode and Visual Studio [1]. It pins the opening line of a scope to the top when it scrolls out of view and it does it multiple levels deep so you can see the class, function definition, conditionals, etc at the top of the source file when browsing deeply nested code. [1] https://learn.microsoft.com/en-us/visualstudio/ide/editor-st...

Okay that’s cool :)

Re: Ada's dependent types, and its types as a whole

#115

Post by mlinksva »

jonlong wrote: post #15

Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history…

I made some small changes based on your comment https://en.wikipedia.org/wiki/Talk:Dependent_type#Ada2012 but I hope you or others with more knowledge improve the page! ~~~~

Re: Ada's dependent types, and its types as a whole

#116

Post by pjmlp »

quietbritishjim wrote: post #109
pjmlp wrote: post #79

Earlier quoted context omitted.

https://www.gnu.org/software/gnat/

The original point is that there is only one open implementation. This is a link to that one open implementation. You are pushing this conversation around in circles.

How many open implementations are there for plenty of other languages, like the main implementations, driving the whole ecosystem, not partial implementations with if and buts?

Re: Ada's dependent types, and its types as a whole

#117

Post by nmilo »

alexvitkov wrote: post #75
fpoling wrote: post #65

Earlier quoted context omitted.

Explicit language support is very nice as the compiler can and do a lot of optimizations and free the space as early as possible on all control paths and ensure full memory safety. For example, when a function returns a thing on the second stack the compiler can arrange that, before returning, the thing is moved to the second stack position that was at the start of the function. This releases the memory that was used…

Doing frees/moves/copies on the second stack makes it harder to track the lifetime of allocations, and restricts what you can use it for - to free a block on the stack you necessarily have to free everything after it. Most programs have a point where you know nothing on it is used and it's convenient (and very performant) to free the entire thing, and that makes it way easier to reason about - when you alloc from it…

You can just pop the second stack at each function return, though that does limit its use to only really scratch-space for dynamically sized objects. Like this: https://nullprogram.com/blog/2023/09/27/. “Arenas” are passed by value so their end pointer will auto reset when the function returns.

Re: Ada's dependent types, and its types as a whole

#118

Post by chlorion »

nytpu wrote: post #80
Keyframe wrote: post #42

Earlier quoted context omitted.

Ada is a lot of fun and a great thing which is ruined (and blessed) by the fact there's de facto only one implementation and company behind it out in the open, and that is semi-closed / license PITA. There were improvements over the years by AdaCore, but I think this altogether hurt the adoption of such a great language in general - no other wide open implementation (like Rust has). If you want to see an extreme exam…

It's FOSS and is actually included with GCC, but the toolchain is still a PITA to install just because no one (other than Debian and Arch Linux) bothers packaging it. I think Alire is supposed to make it easy to install but I haven't used it much: https://alire.ada.dev/ SPARK 2014 itself is the same too AFAIK, the problem is there's a lot of auxiliary static analysis tools and plugins that are gated behind AdaCore's…

I'm pretty sure that gentoo also packages ada, but it doesn't get installed by default, as its behind a USE flag.

Re: Ada's dependent types, and its types as a whole

#119

Post by kevlar700 »

Keyframe wrote: post #92
wavemode wrote: post #76

Earlier quoted context omitted.

Why would the license of the compiler matter? It doesn't require you to license the code you compile with it accordingly.

runtime matters

Why? The code you compile isn't infected by the runtime license?

Re: Ada's dependent types, and its types as a whole

#120

Post by kevlar700 »

Yoric wrote: post #104
zozbot234 wrote: post #45

Earlier quoted context omitted.

I would quibble with the "fairly easily" part. It will likely become possible to make them as ergonomic as the Ada variety if Rust's const generic and constant evaluation facilities are extended far enough, but this would also open up the can of worms of essentially giving Rust the full capabilities of a dependently-typed language (at least in its compile-time subset), which Rust's dev community may not necessarily b…

I'll grant you that Rust is not nearly as ergonomic as Ada in this domain, but doing it manually is fairly easy. Turning it into a library is a bit more complicated - these days, I'd do it with macros. Of course, making sure that the compiler knows about it for optimization purposes would require lots of const generic.

The real benefit of Adas typing is that it is so easy to utilise often preventing logic errors.
Post reply on HN