3 ms·

> What I meant was that it seems to matter to you what name you give your language. I don't care about the name: you could call both languages “Java” (just lik

> What I meant was that it seems to matter to you what name you give your language. I don't care about the name: you could call both languages “Java” (just like two different people could be called “John”), as long as we're all aware that they're two languages and it's clear from context which one we're talking about. > Do you have examples? let x: int = 97 let p: is_prime x = <proof-that-97-isn't-divisi...>

pron 10y ago
That's not what I meant. Can x be a function, and can you then prove a proposition about x in a different module/in the same module in a different definition? E.g., can x be a sorting function whose type specifies that the result is sorted, and can you then have another proposition specifying that the result is also stable?
- catnaroek 10y ago
  > That's not what I meant. Can x be a function, and can you then prove a proposition about x in a different module/in the same module in a different definition? Well, in my previous example I used an `int`, but there's no fundamental reason why you couldn't use a function (or any other type) instead. let f : list int -> list int = <mergesort> let p : (forall x. is_sorted (f x)) = <proof> In this example, `f` itself doesn't have a dependent type, and everything I want to prove about it is proved separately. But you can also do: let f : list (int * int) -> sorted_list (int * int) = <mergesort-sorting-by-first-int> let p : is_stable f = <proof-that-it-respects-the-relative-ordering-of-second-ints-amongst-entries-with-equal-first-ints> In this example, `f` contains a baked-in proof of one fact (that it sorts), but there's another fact that's proved separately (that it's stable). In general, the proof `p` needs access to the definition of `f`. So if `f` is held abstract (its definition isn't exposed to other modules), `p` has to be in the same module as `f`. In most programming languages, with respect to modularity, you only get two options: (0) Keep a value private. (Not expose it.) (1) Expose the existence of a value, indicating its type. Dependently typed languages give you a third option: (2) Expose the full definition of a value. As in, let developers of other modules know that `x` isn't just “a” function (or int or whatever) - it's this particular function (or int or whatever).
  - pron 10y ago
    Got it, thanks! See my other comment explaining how programs and propositions about programs are the same thing (and are artificially separated by the designer of the language).

pron 10y ago

That's not what I meant. Can x be a function, and can you then prove a proposition about x in a different module/in the same module in a different definition? E.g., can x be a sorting function whose type specifies that the result is sorted, and can you then have another proposition specifying that the result is also stable?

catnaroek 10y ago
> That's not what I meant. Can x be a function, and can you then prove a proposition about x in a different module/in the same module in a different definition? Well, in my previous example I used an `int`, but there's no fundamental reason why you couldn't use a function (or any other type) instead. let f : list int -> list int = <mergesort> let p : (forall x. is_sorted (f x)) = <proof> In this example, `f` itself doesn't have a dependent type, and everything I want to prove about it is proved separately. But you can also do: let f : list (int * int) -> sorted_list (int * int) = <mergesort-sorting-by-first-int> let p : is_stable f = <proof-that-it-respects-the-relative-ordering-of-second-ints-amongst-entries-with-equal-first-ints> In this example, `f` contains a baked-in proof of one fact (that it sorts), but there's another fact that's proved separately (that it's stable). In general, the proof `p` needs access to the definition of `f`. So if `f` is held abstract (its definition isn't exposed to other modules), `p` has to be in the same module as `f`. In most programming languages, with respect to modularity, you only get two options: (0) Keep a value private. (Not expose it.) (1) Expose the existence of a value, indicating its type. Dependently typed languages give you a third option: (2) Expose the full definition of a value. As in, let developers of other modules know that `x` isn't just “a” function (or int or whatever) - it's this particular function (or int or whatever).
- pron 10y ago
  Got it, thanks! See my other comment explaining how programs and propositions about programs are the same thing (and are artificially separated by the designer of the language).