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

71–80 of 146 posts

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

#71

Post by zozbot234 »

4ad wrote: post #68

I am not versed in Ada, but Ada does not seem to have dependent types at all, in fact the author doesn't seem to understand what dependent types are. All his examples seem to revolve about arrays and bounded integers so I will stick to those example (although DT are far richer than that). In a language with dependent types you don't merely have arrays with arbitrary bounds, but you get a proof that array access is al…

> you get a proof that array access is always within bounds

But the way you get 'proofs' in dependently-typed languages is just by building a tree of function evaluations that demonstrate a given logical inference at compile time, and that disappear (are translated to a unit type) when 'program extraction' is performed on the code. This is ultimately a kind of meta-programming. And in a DT language you would still need runtime checks within your extracted code to ensure that program inputs provided at runtime satisfy the logical conditions that the "proof" part of the program relies on: the need for runtime checking is thus reduced to a bare minimum, but not fully eliminated.

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

#72

Post by lenkite »

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 never even knew that this "Ancient Language" had dependent types. Always thought it was a "modern" invention of snazzy newer academic languages like Idris, etc.

But, its easy to figure out why it didn't become popular. C/C++/any other top10 language all had free compilers available to everyone. Ada didn't during the explosive era of computing expansion. Also, not a problem nowadays with IDE auto-complete/snippets but the language was too verbose for older generation of programmers.

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

#73

Post by ajdude »

zerr wrote: post #29
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 literally verbose syntax contributes to its unpopularity as well. It is extremely hard to skim/read and comprehend prose-like Ada code.

For me it's the other way around, I can skim a program written in Ada and figure out what it's doing almost the immediately because it is highly structured and enforces correctness with no ambiguity through its syntax.

I can't really do the same for rust which tends to lend itself into a more confusing format.

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

#74

Post by ajdude »

For anyone interested in trying Ada, I've written an installer brings in the entire tool chain with a copy and paste command line on macOS and Linux: https://getada.dev

Here is some previous discussion:

Show HN: Getada: rustup-like installer for Ada's toolchain/package manager 194 points | 115 comments: https://news.ycombinator.com/item?id=40132373

There is a quickstart with a link to a large tutorial: https://www.getada.dev/how-to-use-alire.html

If you wanna try out Ada without even installing anything, you can also check out https://learn.adacore.com/

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

#75

Post by alexvitkov »

fpoling wrote: post #65
alexvitkov wrote: post #35

Earlier quoted context omitted.

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 a…

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 know your block of memory it's valid until a point:

  - For a video game you can  at the start of every frame
  - For a web server you can alloc a new stack for every incoming request and  after the request is over
  - For a short-lived program you may not even need to  at all

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

#76

Post by wavemode »

Keyframe wrote: post #64
LiamPowell wrote: post #43

Earlier quoted context omitted.

As far as I'm aware, the compiler AdaCore sells is just GCC. You can install GCC built with Ada support from your distros package manager and it will just work. You can also download builds from here: https://github.com/alire-project/GNAT-FSF-builds

If something hasn't changed, FSF builds are a year behind libre version (by design), and libre version is GPL3 cancer which is not suitable for commercial development. You're then stuck either with a year old version or buy into AdaCore Pro version of it. Not great, not terrible.. but that's kind of the only game out in the open, which is what makes it different from most of other languages out there.

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

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

#77

Post by 4ad »

zozbot234 wrote: post #71
4ad wrote: post #68

I am not versed in Ada, but Ada does not seem to have dependent types at all, in fact the author doesn't seem to understand what dependent types are. All his examples seem to revolve about arrays and bounded integers so I will stick to those example (although DT are far richer than that). In a language with dependent types you don't merely have arrays with arbitrary bounds, but you get a proof that array access is al…

> you get a proof that array access is always within bounds But the way you get 'proofs' in dependently-typed languages is just by building a tree of function evaluations that demonstrate a given logical inference at compile time, and that disappear (are translated to a unit type) when 'program extraction' is performed on the code. This is ultimately a kind of meta-programming. And in a DT language you would still ne…

> This is ultimately a kind of meta-programming.

There is connection between advanced type systems and metaprogramming, you don't even need dependent types to reach it, GHC can express, for example, typed symbolic differentiation of compiled terms[1], something that would be of interest to a Lisp programmer. This is not a surprise, System Fω has a copy of simply typed lambda calculus at the type level.

> But the way you get 'proofs' in dependently-typed languages is just by building a tree of function evaluations that demonstrate a given logical inference at compile time, and that disappear (are translated to a unit type) when 'program extraction' is performed on the code.

As someone who works on dependently-typed language, I have no idea what you mean. Programs in most DT languages run directly (Lean, Idris, Adga, etc), code extraction is a Coq thing (and Isabelle, but Isabelle does not use DT). Some languages have type erasure, some don't. Some are explicitely concerned about type erasure (Idris), some don't.

> And in a DT language you would still need runtime checks within your extracted code to ensure that program inputs provided at runtime satisfy the logical conditions that the "proof" part of the program relies on: the need for runtime checking is thus reduced to a bare minimum, but not fully eliminated.

In a typed language you need to parse the input exactly once and construct a typed term. The type system itself will prevent you from constructing an ill-typed term -- that is, the parsing routine itself is typed checked (at compile time). Yes, parsing needs to happen, this is true for any language, not just a DT one, but the act of parsing itself produces a dependently-typed term, there are no additional checks happening on the term while it is being used at runtime. The fact that a parsed term cannot, for example, cause an integer overflow inside your program no matter what is quite a massive guarantee.

[1] https://mail.haskell.org/pipermail/haskell/2004-November/014...

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

#79

Post by pjmlp »

mirashii wrote: post #57
pjmlp wrote: post #52

Earlier quoted context omitted.

Not at all, there are 7 Ada compiler vendors still in business. https://www.adacore.com/ https://www.ghs.com/products/ada_optimizing_compilers.html https://www.ptc.com/en/products/developer-tools/apexada https://www.ddci.com/products_score/ http://www.irvine.com/tech.html http://www.ocsystems.com/w/index.php/OCS:PowerAda http://www.rrsoftware.com/html/prodinf/janus95/j-ada95.htm And AdaCore sponsors GNAT, with Ada be…

> out in the open This part was an important part of the sentence you might've missed.

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

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

#80

Post by nytpu »

Keyframe wrote: post #42
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…

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 sales wall (and of course they'd never deign to sell licenses affordable to individuals)

Post reply on HN