A first feature is the ability to define “interesting” types. By interesting I mean “generic” types which do things depending on the types of their arguments. In other words, a way to have functions at the type level. In Haskell you can do this with type families. I don’t know if you can do something similar in rust (have a type in a trait and then implement that trait in certain cases to get your function from input type to the type in the trait implementation for the input type)
A second feature that I think is needed is a way to go between types and values which I don’t think rust or swift can do.
Two fundamental dependent types are the dependent sum and dependent product. The dependent product is the type of a function whose output type depends on its input value. This is a generalisation of the product type: the product type (a,b) is like the dependent product type (x:{1,2}) -> T x where T 1 = a and T 2 = b.
The dependent sum type consists of a tag value of some type and a value whose type depends on the tag. For example a vector of arbitrary length Of floats could be written with a type something like:
Sum(n:Nat)(Vec n Float)
And a value like
(2,[1,2])
Sometimes you see online that every pair can be represented as a dependent sum and this is true but completely misses the point because it implies that you should think of it like a generalised product which you should not do.
You can, in fact, use traits to do type-level programming in Rust[1], but this is type-level programming; it isn't /dependent/ types. The biggest "blocker" for using dependent types is that programs must be /total/, because that program has to be evaluated for it to typecheck! If a program is not total, the typechecker has the potential of getting stuck. The two dependently-typed languages I've programmed in, Mostly Agda and a tiny bit of Idris, have totality checkers to aid in this. Generally this means that recursion is only allowed if its structural, and there can be no run-forever loops, i.e., no servers.
I think instead, for one of these languages, the ideal would be opt in should you need it. Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not. You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.
The biggest "blocker" for using dependent types is that programs must be /total/, because that program has to be evaluated for it to typecheck!
Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact!
Generally this means that recursion is only allowed if its structural, and there can be no run-forever loops, i.e., no servers.
You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.
Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not.
This doesn't make a whole lot of sense to me. Dependent types are "proof carrying" in the sense that any program of the type:
Int -> Int
Is a proof that there exists a function of type `Int -> Int`, nothing more. I don't know what "opting out" of the "carrying" there would mean.
You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.
You can be total over IO, and effects do not imply non-totality either.
Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact!
Absolutely, the talk I linked to gets at this to some extent. In rust, partiality causes type checking to fail. You could use it on purpose!
You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.
For sure, but the totality checker is appeased by sized-types, or at least that's how I know to do it in Agda. I've heard it can be done without them, but I'm not familiar with the approach. This is what I intended w/r/t structural recursion.
This doesn't make a whole lot of sense to me.
This is because, as the authors state, to type check the program is to evaluate it, so before it can run you have proof that it is correct.
By opting out I'm more talking about the converse, to opt in when you need it. Kind of the opposite of Idris's %partial directive.
You can be total over IO, and effects do not imply non-totality either.
Hm, that's not how I'm reading this. An infinite loop is, by definition, partial. What I'm gathering from this is that that stuckness that the typechecker can encounter in the face of partiality is okay in Idris, that its typechecker just says, "welp, this is as far as I go."
I’m specifically talking about the “Produces a non-empty, finite, prefix of a possibly infinite result” part on that page. As long as your server generates finite responses in finite times, Idris recognizes your code as total.
When dealing with corecursion (infinite streams) you don't care about whether you terminate, but rather, whether the infinite stream is _productive_ meaning it doesn't stop producing values. The prime example of a function that's impossible(?) to prove productive (for all cases) is filter – since it takes a predicate function that decides whether values are returned or not. If you give filter a predicate that always returns false you will never produce any values, hence that wouldn't be productive.
A first feature is the ability to define “interesting” types. By interesting I mean “generic” types which do things depending on the types of their arguments
LF does not have higher kinded types but it does have dependent types.
Comments
A first feature is the ability to define “interesting” types. By interesting I mean “generic” types which do things depending on the types of their arguments. In other words, a way to have functions at the type level. In Haskell you can do this with type families. I don’t know if you can do something similar in rust (have a type in a trait and then implement that trait in certain cases to get your function from input type to the type in the trait implementation for the input type)
A second feature that I think is needed is a way to go between types and values which I don’t think rust or swift can do.
Two fundamental dependent types are the dependent sum and dependent product. The dependent product is the type of a function whose output type depends on its input value. This is a generalisation of the product type: the product type (a,b) is like the dependent product type (x:{1,2}) -> T x where T 1 = a and T 2 = b.
The dependent sum type consists of a tag value of some type and a value whose type depends on the tag. For example a vector of arbitrary length Of floats could be written with a type something like:
And a value like Sometimes you see online that every pair can be represented as a dependent sum and this is true but completely misses the point because it implies that you should think of it like a generalised product which you should not do.You can, in fact, use traits to do type-level programming in Rust[1], but this is type-level programming; it isn't /dependent/ types. The biggest "blocker" for using dependent types is that programs must be /total/, because that program has to be evaluated for it to typecheck! If a program is not total, the typechecker has the potential of getting stuck. The two dependently-typed languages I've programmed in, Mostly Agda and a tiny bit of Idris, have totality checkers to aid in this. Generally this means that recursion is only allowed if its structural, and there can be no run-forever loops, i.e., no servers.
I think instead, for one of these languages, the ideal would be opt in should you need it. Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not. You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.
[1] https://dpitt.me/talks/tt-for-rust/
[2] http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf
Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact!
You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.
This doesn't make a whole lot of sense to me. Dependent types are "proof carrying" in the sense that any program of the type:
Is a proof that there exists a function of type `Int -> Int`, nothing more. I don't know what "opting out" of the "carrying" there would mean.You can be total over IO, and effects do not imply non-totality either.
Absolutely, the talk I linked to gets at this to some extent. In rust, partiality causes type checking to fail. You could use it on purpose!
For sure, but the totality checker is appeased by sized-types, or at least that's how I know to do it in Agda. I've heard it can be done without them, but I'm not familiar with the approach. This is what I intended w/r/t structural recursion.
This is because, as the authors state, to type check the program is to evaluate it, so before it can run you have proof that it is correct.
By opting out I'm more talking about the converse, to opt in when you need it. Kind of the opposite of Idris's %partial directive.
That's fair, you're right. This is poorly stated.
Idris does support forever loops or servers without losing totality. See https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.h...
Hm, that's not how I'm reading this. An infinite loop is, by definition, partial. What I'm gathering from this is that that stuckness that the typechecker can encounter in the face of partiality is okay in Idris, that its typechecker just says, "welp, this is as far as I go."
I’m specifically talking about the “Produces a non-empty, finite, prefix of a possibly infinite result” part on that page. As long as your server generates finite responses in finite times, Idris recognizes your code as total.
When dealing with corecursion (infinite streams) you don't care about whether you terminate, but rather, whether the infinite stream is _productive_ meaning it doesn't stop producing values. The prime example of a function that's impossible(?) to prove productive (for all cases) is filter – since it takes a predicate function that decides whether values are returned or not. If you give filter a predicate that always returns false you will never produce any values, hence that wouldn't be productive.
If you have codata you can have infinite loops in total functional programming.
https://en.wikipedia.org/wiki/Corecursion
LF does not have higher kinded types but it does have dependent types.