5 ms·

You can always use let (in that our case def) to minimize the problem with inlining. I think functional programmers get used to big expressions because they do

You can always use let (in that our case def) to minimize the problem with inlining. I think functional programmers get used to big expressions because they do not inspect every symbol when they are reading, the context gives enough information! But you are correct, I couldn't make it better than its syntax/semantics because the implementation should be also very simple. And yes, PomPom is very simple compared to other proof assistants (we are not dealing only with functional programming but also dependent types).

caotic123 5y ago
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.
saithound 5y ago
I think you made good trade-offs regarding the syntax. Your language needs to be simple in the sense that it should not be complicated to parse unambiguously. But it also had to remain somewhat usable. I think you made a good choice: it's easy to parse, and not all that difficult to read for the people who are likely to use it, after some minutes of deliberate practice. Sure, it's quite symbol-heavy, and it's not as clean as, say, Agda or Idris. But (after a few minutes of practice) I find the difficulty entirely comparable to reading Coq. Unsurprisingly, people who by their own admission never use functional, much less dependently typed, programming languages won't find it easy to read. But nothing you can do would make it easy to read for them, any more than you can make Jack Sprat easy to read for those who do not speak any English. To convey what it does, you'd have to write it in an entirely different language, and it would lose its very purpose in the process.

caotic123 5y ago

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.

saithound 5y ago

I think you made good trade-offs regarding the syntax. Your language needs to be simple in the sense that it should not be complicated to parse unambiguously. But it also had to remain somewhat usable. I think you made a good choice: it's easy to parse, and not all that difficult to read for the people who are likely to use it, after some minutes of deliberate practice. Sure, it's quite symbol-heavy, and it's not as clean as, say, Agda or Idris. But (after a few minutes of practice) I find the difficulty entirely comparable to reading Coq. Unsurprisingly, people who by their own admission never use functional, much less dependently typed, programming languages won't find it easy to read. But nothing you can do would make it easy to read for them, any more than you can make Jack Sprat easy to read for those who do not speak any English. To convey what it does, you'd have to write it in an entirely different language, and it would lose its very purpose in the process.