Dependent type systems

[dabrahams]

@GunpowderGuy raised the topic of dependent type systems, suggesting that Idris2 had some innovations that make dependent types easier to use, and that automated proof systems could be easily built upon them. They offered to elaborate if we opened a thread for the topic, so here we are.

[GunpowderGuy]

Sorry for the late ( and incomplete ) reply, i am currently in a horrible time crunch.

In the previous thread you asked why i mentioned dependent types under meta-programming. They are a kind of type system that allows meta-programming to generate generic programs in the traditional sense. But also programs that are generic across invariants you define with the type system.

lets see a classic example

#include <iostream>
#include <string>
#include <type_traits>

// Primary template
template<bool B>
struct ExampleFunction;

// Specialization for true
template<>
struct ExampleFunction<true> {
    using type = int;  // Type A for true
    static type getValue() {
        return 42;
    }
};

// Specialization for false
template<>
struct ExampleFunction<false> {
    using type = std::string;  // Type B for false
    static type getValue() {
        return "Hello, world!";
    }
};

int main() {
    ExampleFunction<true>::type valueTrue = ExampleFunction<true>::getValue();
    ExampleFunction<false>::type valueFalse = ExampleFunction<false>::getValue();

    std::cout << "Value (true): " << valueTrue << std::endl;
    std::cout << "Value (false): " << valueFalse << std::endl;

    return 0;
}

and in idris2

module Main

%default total

boolDependentFunction : (b : Bool) -> if b then Int else String
boolDependentFunction True = 42
boolDependentFunction False = "Hello, world!"

main : IO ()
main = do
  printLn (boolDependentFunction True)
  printLn (boolDependentFunction False)

As for user defined invariants. In a language like c++ you can define types that depend on types or values ( like std array ). However dependent type systems bridge gaps for you allowing things like a pair of arrays with size unknown at compile time, but of provable equal value. Or functions with an output smaller than the input ( which can be used to prove the totality of functions )

https://github.com/stefan-hoeck/idris2-tutorial/blob/main/src/Tutorial/Dependent.md

This not only enables extra security but also supercharges meta-programming

[dabrahams]

OK. So, the term you're after is multi-phase compilation

No thanks, I meant what I said. People have been using that term in compilers for decades. https://learn.microsoft.com/en-us/cpp/preprocessor/phases-of-translation?view=msvc-170 for example

[hosseinhaeri]

Sorry @dabrahams for it taking me a few days to come back to you. I was detained elsewhere.

the only way to do anything resembling generic programming with it (e.g. treat lists of integers the same way as lists of types)

(The boldfacing is mine.) That property you're after is what is colloquially called "universal polymorphism" in the community of programming languages. This has been a source of attention since Stretchy's seminal work back in 1967. What confuses me is that universal polymorphism seems to somehow relate in your mind (and in Hylo?) to the phase of type-checking templates, as you put it here:

This is specifically about having entities that can effectively contain type errors, but can't be type checked. That's what a template is: it can't be type-checked; only its instantiations can.

For your information, both C++ Concepts and Haskell Type-Classes implement "ad-hoc polymorphism" (as opposed to universal polymorphism). But, C++ templates have the property you outline above; whereas type-checking of type-parameterised code in Haskell is performed at the definition site (which is apparently what you like in Hylo). So, I fail to see the relationship between universality and definition-site type-checking. Would you mind explaining the relationship please? (See this work of Jeremy Gibbons with few hits on the ad-hocness of both C++ Concepts and Haskell Type-Classes.)

The other thing which I am unclear about is the reason why you consider template instantiation time the runtime of C++TMP.

... which basically defers all type checking until TMP runtime (i.e. when templates are instantiated)

Template instantiation is nothing but a function application during compile-time of C++. But, function application per se needs not to take place during the runtime of a language. For example, in ordinary C++, constexpr functions (when passed constexpr arguments) and consteval functions (unconditionally) get invoked too but during compile-time.

So, even though -- contrary to my previous words -- I admit that concept enforcement takes place only after instantiation, the following quote from cppreference that you yourself brought up...

Violations of constraints are detected at compile time, early in the template instantiation process

... suggests that it makes perfect sense to take that early phase the compile-time of C++TMP, and, hence, C++ Concepts the static semantics of C++TMP.

[dabrahams]

I only raised lack of polymorphism as an example of the weakness of TMP's static type system. I consider instantiation time the runtime of TMP because it's when the compile-time computation, e.g. of new types, happens. constexpr and consteval stuff is not TMP—it doesn't even necessarily involve templates—but unlike template metaprograms, definitions marked constexpr and consteval are separately typechecked, independent of whether they are used anywhere…as long as those definitions are not templates ;-)

suggests that it makes perfect sense to take that early phase the compile-time of C++TMP, and, hence, C++ Concepts the static semantics of C++TMP.

Sorry to be blunt, but that is just wrong. Template instantiation, and thus concept checks, take place during the evaluation of (compile-time) expressions. Static type checking is something we apply to definitions without having to evaluate expressions depending on those definitions. Dynamic type checking is what happens when type soundness is validated as a consequence of the evaluation of expressions. To the extent that adding C++ concept constraints to templates makes any checking happen earlier, it is the compile-time equivalent of the assertion in this Python:

x = [1, 2, 3, 4]
def inner(i):
  return x[i]
  
def outer(i):
  assert type(i) is int, "concept check failed"
  return inner(i)
  
print(outer("foo"))

The program would fail without this assertion, but we'd get a longer error backtrace from Python. This backtrace corresponds exactly to a template instantiation backtrace in C++, which can be shortened by adding concept checks on outer templates.

[emdash]

I have a couple larger examples that might be more interesting. I'm happy to elucidate how they work (insofar as I understand it) for those who don't read the notation.

Dates

Here's an example which captured my attention early: https://github.com/emdash/idris-datetime/blob/main/src/Date.idr

The heart of it is a dependent record for dates which makes it impossible to represent an invalid date, like 2023-2-29, or 2024-11-31:

export
record Date where
  constructor MkDate
  year:  Nat
  month: Month
  day:   Month.Day (IsLeapYear year) month

The rest of the library does involve the kind of "jumping through hoops" to satisfy predicates that I suspect Hylo devs want to avoid, but I chose to go through this exercise. This shows how dependent types can get a bit ugly.

Dimensional Analysis

https://github.com/emdash/ampii/blob/main/src/Measures.idr

This is a toy dimensional analysis system. It's not maximally generic. It doesn't handle all the fundamental units. But I think it shows how pleasant dependent types can be.

[dabrahams]

We are well aware of these examples. The use of templates for dimensional analysis goes back to Barton & Nackman, well before standardization. https://www.amazon.com/Scientific-Engineering-Introduction-Advanced-Techniques/dp/0201533936?dplnkId=da1334c3-16c6-4100-b36e-75e68e580bc2&nodl=1

We intend to cover these use cases; The features required are not what we have concerns about when it comes to "dependent type system support"

[waydan]

I've been wondering after reading this: is there something dependent types gets you that isn't available in design by contract? AFAICT, expressing that a value cannot be greater than the input is a post-condition. I don't have experience with languages like idris2, but I've seen dependent types used to constrain valid input which looks a lot like preconditions.

[dabrahams]

🍏 🍎 and 🍊 🍊. DbC is a methodology and dependent types are a language feature. That feature, like basically all features of static type systems, lets you prove at compile time that certain contracts are upheld. Most features called "DbC support" check contracts at runtime and have no role in the type system.

Then again. I don't see how you could possibly validate input using a (static) type system feature.

HTH

[hosseinhaeri]

DbC is essentially not concerned about the stage at which the contract enforcement takes place. Dependent typing is strictly concerned about compile-time.

More to the point: Not everything in dependent typing is about correctness (by contract). A whole world of optimisation only surfaces in the presence of such expressiveness. Expression templates are the closest that C++TMP gets to wrt optimisation, for example. The gist of it is that, when your compiler knows more about your code at compile-time, it can optimise things much better. And, my little research about Hylo is that it's a systems programming language. Such languages are expected to be speed-thirsty. You'd want to jump on such optmisations, I guess.

[emdash]

Hot take: Numbers in types are the "gateway drug" of dependent typing. Once I saw the value of this, I wanted more.

For me, Frankly, it was C++ templates that sent me down the rabbit hole of dependent types. It was C++ that put the concept in my head, but for now I'm quite keen on learning Idris.

I think anyone who's spent any serious time with modern C++ has started to form some intuitive notion of dependent types. The trouble with pointing to C++ as an example of anything is that C++ is, to put it delicately, a legacy language. So it's not the clearest expression of the idea.

Template instantiation, and thus concept checks, take place during the evaluation of (compile-time) expressions. Static type checking is something we apply to definitions without having to evaluate expressions depending on those definitions. Dynamic type checking is what happens when type soundness is validated as a consequence of the evaluation of expressions. To the extent that adding C++ concept constraints to templates makes any checking happen earlier, it is the compile-time equivalent of the assertion in this Python:

x = [1, 2, 3, 4]
def inner(i):
  return x[i]
  
def outer(i):
  assert type(i) is int, "concept check failed"
  return inner(i)
  
print(outer("foo"))

The program would fail without this assertion, but we'd get a longer error backtrace from Python. This backtrace corresponds exactly to a template instantiation backtrace in C++, which can be shortened by adding concept checks on outer templates.

Uh. What? I checked, and assertions throw an exceptions at runtime.

C++ template instantiation may be "morally dynamic", but template instantiation still happens at compile time. That's where this discussion of "phases" comes in. For my part, as a developer and not a compiler author, I don't really care whether the error is found by the compiler itself, or a constraint supplied by a library author, so long as it finds it.

My interset is more about giving library authors the tools needed to produce good libraries, rather than proving everything reduces to lambda terms.

[kyouko-taiga]

Though this conversation is interesting, I am afraid this thread has moved away from its original topic.

We should not be debating the pros and cons of declaration-site checking (e.g., Swift generics) vs use-site checking (e.g., C++ templates) here. I'm happy to explain why we strongly believe the latter is bad and why the end user actually cares, but we should do that in another thread. Anyone feel free to ask the question if you're interested.

[dabrahams]

I have lots to say about that too. But I agree, not in this thread please.

Also, @emdash, I'm going choose to believe you know nothing at all about the history and ongoing professional missions of those you are chatting with; otherwise, I think (or hope anyway) nothing like the implication of that closing sentence would have made it into this thread. Giving library authors the tools needed to produce good libraries is at the heart of the design choices in question.

[emdash]

Fair enough, I do not.

[dabrahams]

Thanks for your participation everyone. I think we failed to set the context for this discussion properly, which resulted in a lot of static, so I am closing it in favor #1200. I hope this helps!