Dependent Type Systems, take 2

[dabrahams]

I'm opening this thread so we can have a more-focused discussion about dependent type systems than the one that arose in #1126, which suffered quite a bit because we failed to frame the discussion in the right way and ask the right questions.

To be clear, we do not consider a type system to be dependent merely by virtue of the fact that numbers (and perhaps other non-type values) can participate in types, as in FixedSizeBuffer<String, 4>. We plan to support that capability—and all the fun use cases that ensue, such as dimensional analysis—in Hylo as a matter of course. What we mean by "dependent type system" is defined by this capability:

the type of the result of a function can depend on the values of the function's function arguments (as opposed to its generic arguments).

A function exploiting that capability might be written like this in Hylo:

/// Returns `n` empty strings.
fun makeBuffer(_ n: Int) -> FixedSizeBuffer<String, n> {
  FixedSizeBuffer<String, n>(everyElement: "")
}

Notice that n is passed as a runtime parameter to makeBuffer but becomes part of the type of makeBuffer's result, FixedSizeBuffer<String, n>.

We are not interested in arguing over this definition of “dependent type system”; please feel free to use the term “Hylo-dependent type system“ to describe the above capability instead if you disagree with our definition.

This capability is one of the distinguishing features of languages like idris2. We are skeptical that supporting this capability in Hylo would be worth its complexity cost, in part because we are not aware of any compelling use cases. But we realize we are not well-versed in what you can do with it, so we'd like to hear about those use cases, and in particular (but not exclusively) how they might be used to build automated proof systems, as @GunpowderGuy suggested was possible.

Thanks everyone!

[emdash]

I am a relative new-comer to Idris, and its sibling languages. I am sharing my outsider perspective, which is closer to that of a C++ or Rust developer than that of a Haskell developer. I have been working with Idris for the past year out of sheer curiosity.

I would agree with @dabrahams' criteria for considering a language dependently typed as the most crucial. Though to that I would add the following, in case the implication isn't clear:

• Arbitrary expressions are syntactically legal in "type position".
• Types are first-class values, of type Type (or some such).
  • You can pass a type to a function
  • you can return a type from a function

I hope this post sets the stage for a more fruitful discussion.

Short Examples

Basic Contrived examples: in hylo-style syntax. (Apologies if what follows isn't quite right, happy to fix if corrected):

constexpr fun ComputedType(x: Bool) -> Type {
  if (x) {
    return int;
  } else {
    return char;
  }
}

fun returns_computed(b: Bool) -> ComputedType<b> {
  if (b) { return 42; } else { return 'c' }; 
}

fun uses_computed(b: Bool, arg: ComputedType<b>) {
 ...
}

struct DependentStruct {
  b: Bool;
  m_computed: ComputedType<b>;
}

The canonical vector append example:

append<T>(a: FixedSizedBuffer<T, m>, b: FixedSizedBuffer<T, n>) -> FixedSizedBuffer<T, m + n> ...

I would add to this is that there is actually no need for T<...>, because there's no syntactic distinction between types and terms. So, for example, ComputedType<b> could be rendered as ComputedType(b). This is essentially how it works in Idris: there's only one syntax for application. This feels natural to me in Idris2, but a bit awkward when translated to a C++-like syntax.

Idris-specific notions

Just to clarify what Idris2's feature set actually looks like.

• GADTs -- user types in idris are a "sum of products"
• Idris provides explicit control over erasure -- you can have unerased types, or explicitly erased values (which overlaps a bit with features like constexpr / consteval in C++).
  • This is a consequence of the particular flavor of dependent type theory Idris uses, known as Quantitative Type Theory or QTT. There are other flavors of dependent type theory which do not have the notion of multiplicity.
  • Idris has opt-in support for linearity via the same mechanism.
• Idris has a notion of implicit arguments
  • Not explicitly part of, or required for, dependent typing. But they are a complementary feature of the language that improves ergonomics for working with proofs.
  • It is also how Idris handles type inference.
• Totality: this is also somewhat overlapping with constexpr / consteval -- a conservative check that a function terminates without crashing on all inputs, this is required for any function used in a "typing context", or in an erased context.
• "elaborator reflection", this is a limited form of direct meta-programming, most commonly used for deriving common interface implementations as is done in Rust.

As a Theorem Prover

It works via the curry-howard correspondence, and you're limited to constructive logic, insofar as I understand such things. A type is read as a proposition, and a function body that type-checks is considered a proof. In Idris, proofs are usually erased.

A simple example of a proposition in Idris2 is NonZero n, where n: Nat. NonZero is just a data type defined in the standard library, and doesn't rely on any special support beyond what's described above.

It's a topic I am still actively studying. Hopefully someone more knowledgeable will chime in.

Real-World Use Cases

My new favorite toy is: https://github.com/stefan-hoeck/idris2-sqlite3, which can satically check that queries conform to the database schema, correctly track types across joins, etc. Still a work in progress, but seems quite promising.

In the mean time, https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md Is the database for Idris2's unofficial package manager, which has some good examples.

They fall into some broad categories:

• allowing for safer APIs which enforce correct usage at the type level
• eliminating the need for runtime state / checks in implementations via type-level guarantees
• eliminating boilerplate or otherwise hairy type-level gymnastics / hacky metaprogramming / external code generators, etc. via type-level computation
• pushing what would otherwise be language-level features into library code
• simplifying the semantics of the language, i.e. most constructs are syntax sugar that expands to a relatively small core language
  • e.g. records desugar to sum types + auto-generated projection functions
  • interfaces are desugared to records / type constraints are desugared to auto implicit arguments

Other flavors of dependent types

• Calclus of Constructions: Used by CoQ and Agda. QTT is an extension of this.
• Refinement Types: see F*, Liquid Haskell and FlowJS. These languages extract logical constraints from type annotations, and hand off the result to an SMT solver. It's less powerful than full dependent typing, but seems more convenient for some tasks. This might be of more interest to hylo than type theories like QTT.
• Observational Type Theory / Homotopy Type Theory: These are active areas of research. Concerned with the problem of "function extensionality" which I take to mean the problem of determining whether two different implementations of a function are "equivalent". This is probably not relevant to hylo, but I could be wrong.

Conclusion

This is getting long, so I'll leave it to future comments and other posters to elaborate on these topics, in particular how Idris2's features dovetail with each other, and what it might mean for hylo.

[emdash]

This one is a bit more of a stretch: A type-safe API for the observer pattern used in UI frameworks, and browser DOM. This assumes some facilities exist for static reflection on types, in particular:

• Function - A subtype of Type restricted to function types
• FunctionArgs : (Type) -> List Type
• FunctionRet : (Type) -> Type

Not suggesting that this is how reflection should work in Hylo, but it's meant to show how dependent types can potentially complement static reflection. This is the kind of thing that FlowJS and TypeScript allow one to do quite naturally, though it looks a little different than presented here.

trait Observable <events: SortedMap<String, Function>> {
  fun emit(
    s: String,
    args: HList<FunctionArgs<events[s]>>
  ) -> FunctionRet<events[s]> { ... }
  fun bind(s: String, callback: events[s]) { ... }
}

type Button : Observable<{"clicked": (Event) -> Bool}> {
  handle_event(e: Event) {
    ...
    if !emit("clocked", [e]) { // <-- type error, "clocked" not in events
       log("event propagation prevented");
       return
    }
    ...
  }
}

fun setup() {
  let b = Button()
  b.bind("clocked", fun (e) { cout << "clicked" }) // <- type error, "clocked" not in events
  b.bind("clicked", fun (e) { cout << "clicked" }) // <- type error: (Event) -> () != (Event) -> Bool
  b.bind("clicked", fun (e) { cout << "clicked" ; return True }) // works
  b.bind("clicked", 42) // type error, 42 is not a function
  ...
}

Idris can probably do this too, but it would likely work a bit differently, and I haven't actually tried to implement it in Idris.

[dabrahams]

Believe it or not, in Idris, s doesn't have to be a static value.

Of course I believe it; that's what the final sentence of the post you're replying to was about. I understand that in that case the parameters to your resulting HList are dynamic, and the static type of the HList is something like HList<D'> where D' is a type (list) synthesized by the compiler to stand in for the result of s.map(ColumnType).

Just showing me examples, though, is not answering my question about the key benefits one gets from the use of dependent types. Maybe you don't understand the question? Answers of the general shape below are the kinds of thing I'm looking for:

• One library can be written that works on both runtime and compile-time inputs, and when it gets compile-time inputs it can produce fully statically typed outputs.
• The library would otherwise have to use type erasure internally to handle the dynamic cases and could at best reconstruct static safety at its API boundary.
• Because the computations done by simple type systems that don't use compile-time function calls are more constrained than what can happen with generalized functions, compilers are able to prove more things about relationships between the results of those computations than they can about generalized function calls, and give better diagnostics when those proofs fail. By pushing runtime values into type form and operating on them with the simple parts of the type system, we can statically ensure things that would otherwise have to be done with assertions, which—even if they fire at compile time—produce a worse experience for users.

(Note that these are my own WAGs; I don't pretend to know the actual answers)

[emdash]

@dabrahams So, to be clear, this is what I am responding to, from @kyouko-taiga:

What I would like to get from this thread is one minimal example of a "thing" that we'd really want but can't achieve without dependent types...

You seem to be asking for way more than that. It's hard to see how I can present something minimal that covers all your bullet points. That seems more like an entire blog post dissecting the sqlite3 library. That might be worthwhile, but it's also not my project.

The Observable example above was meant to show how having dependent types solves a problem with static reflection, namely it saves you from introducing a concrete "value-level" representation of types and the ensuing ugliness around quoting and unquoting. You can just talk about types directly. Type remains opaque, and the reflection API is effectively the API of Type itself. With dependent types, you have a way to type built-in functions with signatures like (Type) -> String, or (Type) -> List<Type>, or (Type) -> Map<String, Type>, etc. I'm not trying to say anything about whether it's legal to operate on types at runtime. My assumption is that type-level computation is generally restricted to compile time.

I understand that in that case the parameters to your resulting HList are dynamic, and the static type of the HList is something like HList<D'> where D' is a type (list) synthesized by the compiler to stand in for the result of s.map(ColumnType).

In Idris, HList is an inductive datatype. What Idris cares about at compile time is some notion of syntactic equality of which my understanding is still a bit shaky. In some cases, Idris will fully compute the type. In others, it doesn't have to, because we're just pattern matching on the variants of HList. I.e it's a "structral" pattern match, with primitive recursion.

One of the difficulties in translating examples from Idris is that Idris uses structural recursion for everything. It makes sense given how Idris is defined. In Hylo, I imagine the same things would be done through compile-time evaluation.

I feel like I've gone as far as I can, especially without knowing more about Hylo itself. I've watched some talks, have been perusing your documentation and specification, and some of the compiler test cases. But examples are sparse and seem a bit contrived in their own right. Where can I find some examples of non-trivial Hylo that's representative of your vision?

By pushing runtime values into type form and operating on them with the simple parts of the type system, we can statically ensure things that would otherwise have to be done with assertions, which—even if they fire at compile time—produce a worse experience for users.

This feels like it's circling back to the point-of-use vs point-of-declaration debate that we're supposed to be avoiding here. I'm happy to discuss that topic elsewhere, or read whatever you have already written on the subject, if you can point me in the right direction.

[dabrahams]

In Idris, HList is an inductive datatype.

Presumably that means HList<A, B, C> can be decomposed into A and HList<B, C> or something? I assumed as much, but what's the relevance of that fact?

What Idris cares about at compile time is some notion of syntactic equality of which my understanding is still a bit shaky.

Presumably that means HList<s.map(ColumnType)> != HList<t.map(ColumnType)> even if s == t, and that you'd need to rely on a runtime check to coerce one into another?

it's a "structural" pattern match, with primitive recursion.

Presumably that mean that pattern matching assertions on your inductive data types can be incorporated into generic constraints?

One of the difficulties in translating examples from Idris is that Idris uses structural recursion… In Hylo, I imagine the same things would be done through compile-time evaluation.

I've not heard the term structural recursion before but what I find when I look it up looks like it's orthogonal to what I understand “compile-time evaluation” to mean. You could have both together or neither. So I'm really unclear on what you're saying here.

Where can I find some examples of non-trivial Hylo that's representative of your vision?

Nowhere, sadly, especially when it comes to things that brush up against the issues of dependent typing. Most of what you'll see in our talks is about the object and mutation models, which are basically orthogonal to these issues. I'm glad you're raising them, because it's getting to the point where we need to nail down the details.

What I can tell you about our vision is:

• We intend to have generic value parameters, so Buffer<String, 10> is a thing.
• Once a generic definition has passed typechecking independent of specific generic parameters, we will never report type errors from within that definition.
• The complete set of constraints to prove any generic typechecks is therefore required as part of its declaration.
• We intend to be able to express things like the concatenation and decomposition of buffers and HLists (which we call tuples). Combined with the previous bullets that means constraints like "the length of this tuple is nonzero" and “the length of this buffer is the sum of the lengths of these other two“ need to be expressible.

I can't speak for @kyouko-taiga , who may have other concerns, but where I'm hesitant to go “full Idris” it mostly has to do with the syntactic equivalence you're referring to above, IIUC:

1. Given that we have mutation, syntactic equivalence is clearly not sufficient for type equality because the meaning of Buffer<n, Int> depends on when you capture n.
2. What are the limits of our symbolic evaluation capabilities, including our ability to reason about relationships between partially evaluated expressions? One of the simplest examples might be, given a generic parameter N, do we know that N + 7 > N + 5? Maybe we need to be able to know that, but there's going to be a limit somewhere. One step up from there: N.adding(7) > N.adding(5), given an appropriate method on Int.
   It's a large design space and I'm keen to limit our capabilities to a useful subset of the possiblities that doesn't overly complicate the design and implementation.

[kyouko-taiga]

This one is a bit more of a stretch: A type-safe API for the observer pattern used in UI frameworks, and browser DOM. This assumes some facilities exist for static reflection on types, in particular:

FWIW, I think this one is a pretty good example. We can encode quite a bit of it with associated types, where clauses, and existentials. What's difficult to represent is the map from event kinds to its associated handler type. I'm not necessarily convinced that one would need this level of specificity, at least not in this particular example, but I can recognize it is a place where you'd have to defer the type check at run-time in Hylo.

The issue is that we have to erase the type of Function to use it in a container. So we can't later recover the precise associated type of each event to type check a call to bind. We can write everything else with our current type system.

[dabrahams]

I just spent a little time looking through TDDI, and found an early example really concerning. Listing 1.4 begins:

StringOrInt : Bool -> Type
StringOrInt x = case x of
                     True => Int
                     False => String
                     
getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
                        True => 94
                        False => "Ninety four"

Now think about how to type-check getStringOrInt. It looks as though seeing the declaration of StringOrInt is insufficient, and the type-checker needs to look into its implementation. Otherwise, how does it know that 94 matches the False case? With that signature, StringOrInt could have been defined to return String in both cases.

To me, it's fundamental that definitions can be type-checked based on the declarations they use, without looking at the corresponding definitions. So this is an example of something I would definitely not want to support in Hylo.

[emdash]

I think you are at least partially correct. But it's also not always the case, and Idris won't always inspect the definition of a type-level function like StringOrInt

One small annoyance: TDDI is written for Idris 1. In Idris2, you would to write

total
0 StringOrInt : Bool -> Type

To:

• opt-in to totality checking
• guarantee erasure,

And only then will Idris2 actually try to evaluate StringOrInt in a typing context. And even then, the body is private to the module where it's defined, unless you also decorate the definition with public export.

If you don't want to expose the implementation of StringOrInt, then you just write export. At that point, only uses like the following are valid:

import StringOrInt

anotherFunction : (x : Bool) -> StringOrInt x 
anotherFunction x = getStringOrInt x

In this case, Idris won't need to, and isn't allowed to, look at the body of StringOrInt.

[emdash]

And the thing I should add, it's the total requirement that is key for satisfying your requirement that you won't see an error message from within StringOrNat. That's because total means "terminates for all input without crashing".* So, you'll never see an error inside StringOrNat because StringOrNat can't crash.

If in the implementation of getStringOrNat you make a mistake, idris will catch it locally:

total
0 StringOrNat : Bool -> Type
StringOrNat True  = Int
StringOrNat False = String

getStringOrNatBusted : (b: Bool) -> StringOrNat b
getStringOrNatBusted True = "foo"
getStringOrNatBusted False = "foo"

- + Errors (1)
 `-- Test.idr line 11 col 28:
     While processing right hand side of getStringOrNatBusted. Can't find an implementation
     for FromString Int.
     
     Test:11:29--11:34
      07 | getStringOrNatWorks True  = 42
      08 | getStringOrNatWorks False = "foo"
      09 | 
      10 | getStringOrNatBusted : (b: Bool) -> StringOrNat b
      11 | getStringOrNatBusted True = "foo"
                                       ^^^^^

* there are some escape hatches useful for working with incomplete code, that you can easily lint for.

[emdash]

And now to satisfy my own curiosity, I did this:

namespace HideBody
  export total
  0 StringOrNat : Bool -> Type
  StringOrNat True  = Int
  StringOrNat False = String

getStringOrNatWorks : (b: Bool) -> StringOrNat b
getStringOrNatWorks True  = 42
getStringOrNatWorks False = "foo"

Which yields (emphasis mine) "Can't find an implementation for Num (StringOrNat True).", and notice how StringOrNat is unapplied in the type error.

- + Errors (1)
 `-- Test.idr line 9 col 28:
     While processing right hand side of getStringOrNatWorks. Can't find an implementation
     for Num (StringOrNat True).
     
     Test:9:29--9:31
      5 |   StringOrNat False = String
      6 | 
      7 | 
      8 | getStringOrNatWorks : (b: Bool) -> StringOrNat b
      9 | getStringOrNatWorks True  = 42
                                      ^^

And as a final note, before I start making dinner, just ignore the specific error messages in this case. They are a little odd because of how Idris treats literal values. Integer literals are passed to fromInteger, which is a method of the Num interface. String literals are passed to fromString, which is a method of the FromString interface. This has nothing to do with the issue at hand, and I'm not looking to defend that particular design choice.

[dabrahams]

I don't think it's helpful to change the names of these functions midstream even if you think StringOrNat is more accurate, and you didn't show a declaration of getStringOrNatWorks; I'm going to assume that you just meant StringOrNat.

I'm clear on what a total function is, thanks. Yes, totality tells you that you won't get a “runtime“ error message about values at compile-time. But non-totality is pervasive and unavoidable and part of math (division, anyone?). If people want to invoke non-total functions at compile-time I'm not inclined to try to stop them; the failures will look “normal,” like runtime errors from an interpreter, and are amenable to familiar tools like debuggers. I'm actually way less concerned about those than I am about getting typing error messages that point to the inside of a function that was already typechecked. Yeah, it's all compile-time evaluation, but the type-checking process is not a user-level abstraction, so it's much harder for them to debug.

[emdash]

I don't think it's helpful to change the names of these functions midstream even if you think StringOrNat is more accurate, and you didn't show a declaration of getStringOrNatWorks; I'm going to assume that you just meant StringOrNat.

Sorry about that, I didn't mean to do that. StringOrInt is the correct name. In practice, it's rare to use Int in Idris, and so Nat just slips out.

. But non-totality is pervasive and unavoidable and part of math (division, anyone?).

True, but this is a whole other kettle of fish we don't need to get into right now.

If people want to invoke non-total functions at compile-time I'm not inclined to try to stop them; the failures will look “normal,” like runtime errors from an interpreter, and are amenable to familiar tools like debuggers.

That's totally fair, but it seems sensible to have special restrictions on functions that get applied in typing contexts.

I'm actually way less concerned about those than I am about getting typing error messages that point to the inside of a function that was already typechecked. Yeah, it's all compile-time evaluation, but the type-checking process is not a user-level abstraction, so it's much harder for them to debug.

I'm trying to show that you don't get this behavior in Idris. The user-facing problem of "errors inside functions which are already type-checked" isn't present in this case, even if your other criterion of "not inspecting the function body" is violated.

I think at least we've arrived at the heart of the matter.

[emdash]

*Note*: Sorry, made the mistake of replying via email and the formatting got utterly mangled, so I've had to manually fix this.

In Idris, HList is an inductive datatype. Presumably that means HList<A, B, C> can be decomposed into A and HList<B, C> or something? I assumed as much, but what's the relevance of that fact?

So, to be clear, it's more like `HList<[A, B, C]>`, there's an "index" of type `List<Type>`. Perhaps it's not as relevant as I first thought. But you're correct. It "decomposes".

What Idris cares about at compile time is some notion of syntactic equality of which my understanding is still a bit shaky. Presumably that means HList<s.map(ColumnType)> != HList<t.map(ColumnType)> even if s == t, and that you'd need to rely on a runtime check to coerce one into another?

Not necessarily. It depends on what `s` and `t` are, and what is known about them in the context of the expression. In some cases, `s` and `t` will indeed unify. In other cases they will not and Idris will throw up its hands. In any case, it's based on some form of local reasoning. There isn't a need for runtime checks or coercion.

it's a "structural" pattern match, with primitive recursion. ... I've not heard the term structural recursion before but what I find <https://craftofcoding.wordpress.com/2021/05/18/recursion-structural-versus-generative/> when I look it up looks like it's orthogonal to what I understand “compile-time evaluation” to mean. You could have both together or neither. So I'm really unclear on what you're saying here.

I probably am getting a bit sloppy here. I have seen this terminology used online. I think you're technically correct. I guess what I should be saying is something like: in Hylo, you'll have "compile-time evaluation" that allows for things like constant folding and evaluation of functions at compile-time. Idris has "unification by normalization" or "unification by evaluation". But this doesn't necessarily mean that type-level terms get fully applied during type checking. Idris will start to normalize type terms until they unify, or don't.

> Where can I find some examples of non-trivial Hylo that's representative of > your vision? Nowhere, sadly, especially when it comes to things that brush up against the issues of dependent typing. Most of what you'll see in our talks is about the object and mutation models, which are basically orthogonal to these issues. I'm glad you're raising them, because it's getting to the point where we need to nail down the details.

Looking forward to it.

What I can tell you about our vision is: - We intend to have generic value parameters, so Buffer<String, 10> is a thing. - Once a generic definition has passed typechecking independent of specific generic parameters, we will never report type errors from within that definition.

I think I see what your concerns revolve around. And now that I know what to look for, I'll keep my eye out for that sort of behavior in Idris.

- The complete set of constraints to prove any generic typechecks is therefore required as part of its declaration.

I think Idris essentially also requires this, but I see your follow-up message and maybe I was wrong about this.

- We intend to be able to express things like the concatenation and decomposition of buffers and HLists (which we call tuples). Combined with the previous bullets that means constraints like "the length of this tuple is nonzero" and “the length of this buffer is the sum of the lengths of these other two“ need to be expressible. Well, that does sound exciting!

Small point of clarification: Idris has a separate notion of tuples. And they are also inductive and heterogenous. But they don't have the list index. So, just to be clear, HList != tuples in Idris.

I can't speak for @kyouko-taiga <https://github.com/kyouko-taiga> , who may have other concerns, but where I'm hesitant to go “full Idris” it mostly has to do with the syntactic equivalence you're referring to above, IIUC: 1. Given that we have mutation, syntactic equivalence is clearly not sufficient for type equality because the meaning of Buffer<n, Int> depends on when you capture n.

I would expect something like this to work: ``` fun makeBuffer(n: Size) -> Buffer<n * 2, Int> { var x = Buffer<n * 2, Int> // syntactic equality is enough here ... initialize buffer ... return x } ``` I don't expect this to work, and I'd be rather impressed if it did. ``` fun makeBuffer(n: Size) -> Buffer<n * 2, Int> { n *= 2 var x = Buffer<n, Int> // probably a type error here ...initialize buffer... return x } ```

1. What are the limits of our symbolic evaluation capabilities, including our ability to reason about relationships between partially evaluated expressions? One of the simplest examples might be, given a generic parameter N, do we know that N + 7 > N + 5? Maybe we need to be able to know *that*, but there's going to be a limit somewhere. One step up from there: N.adding(7) > N.adding(5), given an appropriate method on Int.

What idris does here again is "structural", because at the type level Idris doesn't use `Int`, but `Nat` -- which is a Peano number. So, all Idris needs here is pattern matching, recursion, and a few theorems, and that's sufficient for types like `Vect n a` in Idris. I doubt that's how you want to do this in Hylo.

1. It's a large design space and I'm keen to limit our capabilities to a useful subset of the possiblities that doesn't overly complicate the design and implementation.

So I sense that where you're at is: You feel like you've done your design work on Hylo, and are ready to dive into the rest of the implementation. But you are taking a "last look around" to make sure you don't want dependent types. I feel like it's now or never. If you close the door on dependent types now, you'll have a hard time getting them into the language later if you change your mind. If you allow for the syntax now, I think you can still restrict usage to the cases you want to support. It's just that some things that would have been syntax errors before get caught in a subsequent pass over the parse tree. But then, at least, you're free to gradually relax the rules as the language evolves, without introducing new syntax.

[kyouko-taiga]

I think I see what your concerns revolve around. And now that I know what to look for, I'll keep my eye out for that sort of behavior in Idris.

If we have to ever inspect the body of a function to type check its uses, then that will be a showstopper AFAIC. The problem is not only about having good error reporting. It's also about the ability to hide function bodies from the compiler, not only the developer.

With this constraint, I'm not sure you can structurally reduce type terms until they unify because there'd be nothing to reduce. I think there's a workaround, though. Consider this:

fun string_or_int(_ x: Bool) -> Union<Metatype<Int>, Metatype<String>> {
  // implementation is not available
}

fun get_string_or_int<x: Bool>() -> string_or_int(x) {
  if x { 94 } else { "ninety four" }
}

We could run string_or_int(x) on every return path with the inferred value of x for that path to get the type we're supposed to return. Sadly, while it would work in this very trivial example, I suspect it wouldn't scale.

I don't expect this to work, and I'd be rather impressed if it did.

I think we would have to support this kind of code if we wanted to support dependent or refinement types, otherwise that would split Hylo into two programming "modes". People wanting these dependent features would have to rely on pure functional programming while others would keep using mutable value semantics. Hylo is all about the latter, so that would be a pretty huge loss.

But all hope isn't loss. Without references, I have the intuition that you can mix typestate and mutation. Liquid Rust is on my radar because I think we could do something similar in Hylo in some sort of gradual type system. That's really future work, though.

So I sense that where you're at is: You feel like you've done your design work on Hylo, and are ready to dive into the rest of the implementation. But you are taking a "last look around" to make sure you don't want dependent types. I feel like it's now or never. If you close the door on dependent types now, you'll have a hard time getting them into the language later if you change your mind.

I don't think we're ready to say that we've finished our homework. We have a pretty solid core calculus (which I guess I should formalize at some point ...) and a pretty good understanding of how that calculus can fit into a Swift/Rust-like generic type system, with an important emphasis on declaration site checking. But our design is still malleable.

Regarding dependent-types, our reluctance is really about the tradeoff complexity/gain. We are ready to say no to many features (and have already done so) if we feel they will cost too much complexity. There is value in keeping languages simple, even if that means making some edge use cases harder to write.

For example, many people would say that the obvious comparison point for Hylo is Rust, which has a demonstrably more expressive support for remote parts. But that expressiveness is at the cost of lifetime polymorphism, which we decided was off the table for us.

If you allow for the syntax now, I think you can still restrict usage to the cases you want to support.

We are already accepting any expression in any position. There are no "type expressions" in Hylo, only expressions. So FWIW, I don't think our syntactic choices are closing any door.

[dabrahams]

@emdash wrote:

You feel like you've done your design work on Hylo…but you are taking a "last look around" to make sure you don't want dependent types. I feel like it's now or never. If you close the door on dependent types now, you'll have a hard time getting them into the language later if you change your mind… If you allow for the syntax now… you're free to gradually relax the rules as the language evolves, without introducing new syntax.

IMO you overestimate both how solid we feel the design of the whole language is—especially the values-in-types part—and also how important it is to account for full dependent type capability at this juncture. We're not opposed to adding new syntax to support new features. Finally, don't see that the kinds of features supported by idris2 would demand any new syntax in Hylo. Type expressions are just expressions already; we currently rule out runtime values in type position using a semantic analysis pass after parsing.

[emdash]

I find all of this quite fascinating. I'm definitely keeping my eye on Hylo going forward.

I think we would have to support this kind of code if we wanted to support dependent or refinement types, otherwise that would split Hylo into two programming "modes". People wanting these dependent features would have to rely on pure functional programming while others would keep using mutable value semantics. Hylo is all about the latter, so that would be a pretty huge loss.

And I see why this is a reasonable concern for Hylo, whereas in Idris2 this sort of bifurcation is seen as a feature.

But all hope isn't loss. Without references, I have the intuition that you can mix typestate and mutation. Liquid Rust is on my radar because I think we could do something similar in Hylo in some sort of gradual type system. That's really future work, though.

Can't wait to see it all works out.

We are already accepting any expression in any position. There are no "type expressions" in Hylo, only expressions. So FWIW, I don't think our syntactic choices are closing any door.

Finally, don't see that the kinds of features supported by idris2 would demand any new syntax in Hylo. Type expressions are just expressions already; we currently rule out runtime values in type position using a semantic analysis pass after parsing.

I'm glad at least the syntactic door is left open, and the rest can follow in its own time, if it needs to. Something mentioned earlier let me to believe the situation was otherwise, and so maybe I've been more ardent than was really necessary. Sorry for that.

At least I found one good example, and now I have an idea where to look for others along those lines. Hope I wasn't too annoying. Wasn't trying to be. I'm bowing out of this discussion for now.

[dabrahams]

If we have to ever inspect the body of a function to type check its uses, then that will be a showstopper AFAIC. The problem is not only about having good error reporting. It's also about the ability to hide function bodies from the compiler, not only the developer.

With this constraint, I'm not sure you can structurally reduce type terms until they unify because there'd be nothing to reduce.

My understanding, from reading what @emdash says about export, is that you can think of what Idris2 does with these cases as essentially inlining everything within a module, so for the purposes of checking uses of the function, there is no function boundary. Maybe the inlined parts are taken as a source of truth when it comes to error reporting, but there should be no challenges for the compiler that wouldn't be presented anyway if function calls were disallowed in that use context.

[emdash]

And I agree with this, in a broad sense.