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

31–40 of 146 posts

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

#31

Post by jonlong »

timhh wrote: post #26
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…

Maybe they're not implying this kind of limited dependent type system but surely it is still dependently typed? It's just not the "full fat" dependent typing. Another example of a language with limited dependent typing is Sail. It has "lightweight" dependent types for integers and array lengths (pretty similar to Ada from what it sounds like). It's very good in my experience - it lets you do a lot of powerful stuff w…

Well, "dependently typed" is widely used to mean something like "derived from Martin-Löf type theory, including arbitrary dependent sums and dependent products"; in other words, "dependent types" means "full fat dependent types", and it's the things that are less powerful that require qualifiers.

(So when Sail says it has "lightweight dependent types", that seems fine to me (it does seem to do more than it could with simple types or polymorphic types), but if it simply asserted that it "had dependent types" I would feel misled.)

The wording is subtle and language does change, but what I want to push back on is the confusion I see from time to time that "if I can write anything that looks like a function from values to types, I have the same thing that everybody talking about dependent types has". If you think this you don't know what you're missing, or even that there is something you're missing, and what you're missing is very cool!

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

#32

Post by shakna »

TypingOutBugs wrote: post #25
seabird wrote: post #13

Earlier quoted context omitted.

I've seen a single company that does warehouse management software out of Sweden that advertises (in job listings) that they're using it. Otherwise, it's pretty slim pickings if you're not applying in its wheelhouse (high integrity systems -- aerospace, defense, medical, etc). If you do microcontroller firmware development, I'd say it's perfectly reasonable to float it for a smaller project and just give it a spin. T…

What was the company in Sweden? Thankfully I live in Stockholm!

I think that'd be Lund Sweden, or Consafe Logistics. Similar systems at both.

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

#33

Post by swiftcoder »

shakna wrote: post #30
zerr wrote: post #29

Earlier quoted context omitted.

The literally verbose syntax contributes to its unpopularity as well. It is extremely hard to skim/read and comprehend prose-like Ada code.

Wouldn't Rust's symbol heavy syntax contribute the same?

I think that since a significant portion of Rust developers come from a C++ background, and C++ uses basically the same set of symbols, it's not a huge barrier to adoption

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

#35

Post by alexvitkov »

nmilo wrote: post #3

The 2 stacks is really cool. Seems like it solves a lot of problems dynamic allocation + RAII solves. Is there more written about this?

You don't need explicit language support to do this -- it's a fairly common practice in videogame development, but we usually usually call it an arena/scratch buffer. Ryan Fleury has a wonderful article where goes at length about different memory management strategies [1].

It's just a static buffer that you can use for temporary allocations, e.g. to return an array of 50 int32's to a parent stack frame you can just allocate `50*sizeof(int32)` bytes on that buffer and return a pointer to the beginning, instead of a heap-allocated `std::vector`. Every allocation advances the head of the buffer, so you can have multiple allocations alive at the same time.

Every once in a while you need to free the buffer, which just means resetting its head back to the start - in the case of games the beginning of a new frame is a convenient point to do that.

This doesn't solve dynamic memory in general, as it can't be used for long-lived allocations, it just saves you a bunch of temporary heap allocations. It doesn't solve all problems that RAII does either, as RAII is often used for resources other than memory - files, sockets, locks, ...

[1] https://www.rfleury.com/p/untangling-lifetimes-the-arena-all...

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

#36

Post by LiamPowell »

Ygg2 wrote: post #19
LiamPowell wrote: post #7

Earlier quoted context omitted.

I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does. There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers: 1. Having the option to use SPARK for fully verified code provides a superset of the co…

> I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. Why? Do you program in Ada or Coq? People can't be bothered to track lifetimes, what makes you think they are ready to track pre/post-conditions, invariants and do it efficiently and thoroughly.

Having the option there is good, even if not everyone uses it. The same thing applies to Rust.

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

#37

Post by Yoric »

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…

For what it's worth, many Rust developers (including myself) are also Ada fans.

Note that ranged types, decimal types, etc. can fairly easily be emulated in Rust, with what I find is a clearer error mechanism.

SPARK is, of course, extremely cool :) There are several ways to work with theorem provers and/or model checkers in Rust, but nothing as nicely integrated as SPARK so far.

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

#38

Post by touisteur »

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…

SPARK allows you to statically prove properties about Ada code. Proving a sort implementation is a classic example : https://blog.adacore.com/i-cant-believe-that-i-can-prove-tha...

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

#39

Post by mentalgear »

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…

Ideally, Rust would start adopting excellent features like Ada's SPARK, and vice-versa Ada get inspired by Rust's good parts as well.

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

#40

Post by typ »

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…

The popularity of a programming language is not always about what the language offers. I would say a comprehensive, well-documented, mature set of standard libraries for its target audience is far more important (notable examples like R, Python, and Go). Last time I checked, Ada doesn’t even have a de facto, high quality TLS/crypto library, let alone various essential protocol/format codecs, yet the core team (AdaCore I assume) puts a lot of resources into offering a few sophisticated flagship IDEs that potential hobbyists would never use (they already have vim, emacs or vscode). I understand that as a business they have to sell something for revenue and they cannot sell standard libraries. So, that’s probably a dilemma that we cannot have the nice things for Ada to take off.
Post reply on HN