5 ms·

Also, my current work/job is using Kind as a foundation, the purpose of this language is exactly what you have asked for, give a check on https://github.com/uwu

Also, my current work/job is using Kind as a foundation, the purpose of this language is exactly what you have asked for, give a check on https://github.com/uwu-tech/Kind https://github.com/uwu-tech/Kind.

jimsimmons 5y ago
Cool! No offence, I went on a rant hoping to start a discussion about FP. The fact that you have a dependently typed language in 1000 lines is an amazing feat. Don’t want to take anything away from that. I just wish the functional community took readability more seriously is all
- tluyben2 5y ago
  Maybe it is because of when you are doing this all day, you really don't see this anymore? I can read j/k just fine, as well as Haskell, but I find many imperative languages noisy and basically ugly and unreadable. I like things terse and as much as I can on 1 screen so I don't have to scroll or remember things (when you get older, remembering wtf something was called again gets pretty annoying; very strict static typing and defining types precisely (aka a zipcode or telephone number are not strings!) together with terse functional constructs help a lot; the IDE will know everything so you can focus on implementation).
devit 5y ago
Interesting! Though it seems to share the problem of all current dependently typed languages of not supporting efficient implementation since everything has to be boxed and there are no linear types. So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages.
- zozbot234 5y ago
  AIUI, the integration of linear types (or substructural types in general) with dependent typing is still a matter of research. Even "simple" type system extensions like higher-kinded types come with a lot of added complexity. There is also what's arguably a deeper obstacle to "efficient" implementation of dependent types because dependent typing does away with the phase separation between compile-time and run-time. We do have "program extraction" features in many DT languages to mitigate this, but they're still ad-hoc additions, there isn't yet a principled approach to the issue.
  - AnthonBerg 5y ago
    Idris 2 has quantitative dependent types. As far as I know quantitative types contain linear types. Are a superset. Idris typechecks 0 and 1 uses of types (and many). It’s a great language. https://idris2.readthedocs.io/en/latest/updates/updates.html#new-core-language-quantities-in-types https://idris2.readthedocs.io/en/latest/updates/updates.html... The locus of the research that Idris’ linear types are based on might be Conor McBride’s paper I Got Plenty O’ Nuttin: https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.p... It’s a beautiful paper. There are other papers in between McBride’s paper and the implementation. They’re great papers too. I find it telling that the Idris 2 source code for quantitative types in the Idris 2 compiler is beautifully readable and understandable. This is what tends to happen in Idris code. Clarity.
- erichocean 5y ago
  > So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages. Or…use TLA+, which doesn't have types (but you instead define near-trivial type invariants that the model checker checks). This turns out to have a lot less ceremony, while producing extremely useful results quickly. tl;dr TLA+ is a lot more practical if you care about bug-free software, and not even in the same universe in terms of difficulty as something like Coq. However, Coq can do fancy mathematics that TLA+ doesn't even try to do, so both should exist. (Neither are easy to learn, but TLA+ is much, much easier than Coq.) I'm familiar with Coq, and reach for TLA+ and Alloy for practical programming. Coq is super-interesting, but ultimately not very practical for programming today. It's very nice for doing weird math stuff though. (You can't do any weird math stuff in TLA+.) In the end, it kind of depends where you think you'll get the most bang for the buck with formal verification: can you confidently write correct code, if you get the design right? Or are you afraid that even with a flawless design/spec, you'll still screw up the code? If it's the latter, Coq (and relatives) are what you want, though almost no-one uses the generated (read: provably correct) code. Expect to spend years on anything useful and produce at least one PhD, probably multiple, in the process. It's an absolutely enormous amount of work. OTOH, if you're concerned that your proposed design might have issues, then TLA+ is many, many orders of magnitude more useful in practice, because it can help you produce a correct design with very little effort (days to weeks). TLA+ helps you find specification errors extremely easily, and the specs (once you get used to it) are easy to write. Once the design/spec has been tested to work correctly in TLA+ (using a model checker), you still have to implement it (e.g. in Rust), but honestly, that's straightforward once the spec is correct and your mental model of the problem is solid. Highly recommended.
  - zozbot234 5y ago
    > tl;dr TLA+ is a lot more practical if you care about bug-free software TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq. Usually you build a simplified "toy" model in TLA+ of some architecture of interest, then use model checking to try and refute some claimed properties of that model. If the model checker finds a refutation of some property, then yes, that's a verified bug in your toy model. If it fails to find one, that's not a proof of correctness other than in very special cases where a property can be checked finitely. So yes, model checking is helpful in some cases, but it's not a generally useful tool. And there are ways to do the same things in general proof assistants, e.g. by interfacing them with external SMT tools. The TLA language in itself is also unproblematic, it simply adds modalities for time, state and non-determinism to ordinary logic, and there are well-known ways to convert ("embed") those features to a form that a proof assistant can work with.

jimsimmons 5y ago

Cool! No offence, I went on a rant hoping to start a discussion about FP. The fact that you have a dependently typed language in 1000 lines is an amazing feat. Don’t want to take anything away from that. I just wish the functional community took readability more seriously is all

tluyben2 5y ago
Maybe it is because of when you are doing this all day, you really don't see this anymore? I can read j/k just fine, as well as Haskell, but I find many imperative languages noisy and basically ugly and unreadable. I like things terse and as much as I can on 1 screen so I don't have to scroll or remember things (when you get older, remembering wtf something was called again gets pretty annoying; very strict static typing and defining types precisely (aka a zipcode or telephone number are not strings!) together with terse functional constructs help a lot; the IDE will know everything so you can focus on implementation).

devit 5y ago

Interesting! Though it seems to share the problem of all current dependently typed languages of not supporting efficient implementation since everything has to be boxed and there are no linear types. So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages.

zozbot234 5y ago
AIUI, the integration of linear types (or substructural types in general) with dependent typing is still a matter of research. Even "simple" type system extensions like higher-kinded types come with a lot of added complexity. There is also what's arguably a deeper obstacle to "efficient" implementation of dependent types because dependent typing does away with the phase separation between compile-time and run-time. We do have "program extraction" features in many DT languages to mitigate this, but they're still ad-hoc additions, there isn't yet a principled approach to the issue.
- AnthonBerg 5y ago
  Idris 2 has quantitative dependent types. As far as I know quantitative types contain linear types. Are a superset. Idris typechecks 0 and 1 uses of types (and many). It’s a great language. https://idris2.readthedocs.io/en/latest/updates/updates.html#new-core-language-quantities-in-types https://idris2.readthedocs.io/en/latest/updates/updates.html... The locus of the research that Idris’ linear types are based on might be Conor McBride’s paper I Got Plenty O’ Nuttin: https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.p... It’s a beautiful paper. There are other papers in between McBride’s paper and the implementation. They’re great papers too. I find it telling that the Idris 2 source code for quantitative types in the Idris 2 compiler is beautifully readable and understandable. This is what tends to happen in Idris code. Clarity.
erichocean 5y ago
> So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages. Or…use TLA+, which doesn't have types (but you instead define near-trivial type invariants that the model checker checks). This turns out to have a lot less ceremony, while producing extremely useful results quickly. tl;dr TLA+ is a lot more practical if you care about bug-free software, and not even in the same universe in terms of difficulty as something like Coq. However, Coq can do fancy mathematics that TLA+ doesn't even try to do, so both should exist. (Neither are easy to learn, but TLA+ is much, much easier than Coq.) I'm familiar with Coq, and reach for TLA+ and Alloy for practical programming. Coq is super-interesting, but ultimately not very practical for programming today. It's very nice for doing weird math stuff though. (You can't do any weird math stuff in TLA+.) In the end, it kind of depends where you think you'll get the most bang for the buck with formal verification: can you confidently write correct code, if you get the design right? Or are you afraid that even with a flawless design/spec, you'll still screw up the code? If it's the latter, Coq (and relatives) are what you want, though almost no-one uses the generated (read: provably correct) code. Expect to spend years on anything useful and produce at least one PhD, probably multiple, in the process. It's an absolutely enormous amount of work. OTOH, if you're concerned that your proposed design might have issues, then TLA+ is many, many orders of magnitude more useful in practice, because it can help you produce a correct design with very little effort (days to weeks). TLA+ helps you find specification errors extremely easily, and the specs (once you get used to it) are easy to write. Once the design/spec has been tested to work correctly in TLA+ (using a model checker), you still have to implement it (e.g. in Rust), but honestly, that's straightforward once the spec is correct and your mental model of the problem is solid. Highly recommended.
- zozbot234 5y ago
  > tl;dr TLA+ is a lot more practical if you care about bug-free software TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq. Usually you build a simplified "toy" model in TLA+ of some architecture of interest, then use model checking to try and refute some claimed properties of that model. If the model checker finds a refutation of some property, then yes, that's a verified bug in your toy model. If it fails to find one, that's not a proof of correctness other than in very special cases where a property can be checked finitely. So yes, model checking is helpful in some cases, but it's not a generally useful tool. And there are ways to do the same things in general proof assistants, e.g. by interfacing them with external SMT tools. The TLA language in itself is also unproblematic, it simply adds modalities for time, state and non-determinism to ordinary logic, and there are well-known ways to convert ("embed") those features to a form that a proof assistant can work with.