31–40 of 88 posts
What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
I bought the book "Type Driven Development in Idris" and got several chapters in before getting distracted by whatever else. It was enough that I'm now annoyed relatively often that I can't pass types as parameters to be altered during execution. I really think they're onto something brilliant. I need to pick it back up and finish the book.
What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
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…
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.
I bought the book "Type Driven Development in Idris" and got several chapters in before getting distracted by whatever else. It was enough that I'm now annoyed relatively often that I can't pass types as parameters to be altered during execution. I really think they're onto something brilliant. I need to pick it back up and finish the book.
Hmm. My interest is piqued but this book is from 2017 and I am wondering if it is not horribly out of date at this point. WDYT?
Earlier quoted context omitted.
Guaranteed termination of a sound dependent type system is only useful as a mathematical property, not a practical one (yes, I know the mathematical consequences have practical benefit but I mean directly it doesn’t say anything about what a typical user thinks of as “termination”). You could still trivially write an algorithm at the type level which is Turing-complete in a practical sense. For example, write a type…
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number. To do that you’d first need to be able to fit Graham’s number into your source code which unfortunately is never going to happen. Idris has a termination checker which in practice rejects non-primitive recurs…
Earlier quoted context omitted.
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…
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…
> Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference.
But latter they also go on to say:
> Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme.
I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also possible, is that a new language and a new runtime could enable new optimizations that are not possible before. The author did mention Chez's profiling tools help a lot in the rewrite. So I was curious: is it really true, that we cannot attribute some part of the speedup to language differences?
Also I was interested in the rationale behind using Scheme to replace Haskell, but I failed to find some reasoning behind this, anyone can shed some light on this?
Earlier quoted context omitted.
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…
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…
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
> 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.
The author first goes with: > Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference. But latter they also go on to say: > Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme. I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also p…
The author even says that it's difficult to write C that deals well with the functional style of lots of little functions, and this is a problem Scheme also has and has solved. That's enough rationale to switch to Scheme:
> Generating good C code corresponding to a functional program which might have lots of small (and higher order) definitions is extremely challenging, so it is better to take advantage of someone else's work here.