Get the latest tech news

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

On Ada's Dependent Types, and its Types as a Whole December 27, 2024 So I like to joke occasionally on the Fediverse that when looking at Wikipedia's list of programming languages supporting dependent types: It's tons of extremely complex functional languages, formal theorem provers, and… Ada, a random Government Language dating back to 1983. Also you'll note that at no point in any Ada documentation anywhere do they feel the need to bring up set theory or the λ cube when explaining how dependent types work :P I just love the juxtaposition of the highly formalized academic/research/for-fun languages with a very bureaucratic-feeling language whose design philosophy is very similar to COBOL's.1 But then I'll usually get one of a few functional programmers/type theory people that follow me to ask about Ada's dependent types, and this time I felt the motivation to write a big post explaining dependent types in Ada.

Also you'll note that at no point in any Ada documentation anywhere do they feel the need to bring up set theory or the λ cube when explaining how dependent types work :P And similarly, SPARK had concrete requirements for a specific set of tasks different from what academics want, and it just happened that theorem provers and FP theory can be applied to those problems to great effect. Although I haven't had more than a casual IRC chat with any of the standardizers so maybe they did actually get their ideas directly from type theory and just fit them into a non-academic language, rather than stumbling across the concept like I hypothesize here.

Get the Android app