Replies: 3 comments 7 replies
-
|
Commenting on this. First, Dr. Farmer's (i) and (ii).
Note that substituting proofs for unit tests is not good. As just one example: Noel and I had lots of proofs in our work on definite folds, and yet the behaviour was wrong, something we eventually saw when we ran some tests! It's just that our code and our theorems agreed with each other, but not with what we actually wanted. Indeed, it is true that "dependent types" embody a certain staging discipline which is implicit in a single-stage language (but still present), but quite explicit when doing code generation. So Drasil, being staged, lets us see more. One point (for me) of dependently-typed programming languages is that you can be much more precise in saying what you intend to do. In other words, your types can capture "what you mean" much more closely. Which is very useful when you know what you're doing. When you're still exploring, they can be a funny game. Whether they are suitable for general programming really depends on how much we know about what we're doing. Idris is written in Idris now, after all. But for quite a lot of programming, we still don't know enough to be successful at it! I think the questions to ask are:
|
Beta Was this translation helpful? Give feedback.
-
|
This is very interesting! Thank you! I didn't know that Idris, Agda, nor ATS were able to erase the proofs. That's a very interesting thread! -- by any chance, do you have any paper suggestions regarding these? Regarding (ii)s question: I think that we primarily manipulate the syntax of many well-defined logical structures. I guess this is a kind of programming, but also a kind of logic? Regarding the unit tests v proofs, that's surprising to me, but I think I can see where it might go awry. I think the "staging discipline" is approximately what I was trying to get at with my post. In some sense, we also erase some kinds of "proofs" when we compile our knowledge-bases to, say, Java. Those proofs also allow us to implicitly assume things that might be otherwise unsafe in manual Java development. For example, when we have functions with multiple return-values, we place them in a "Object[]", and all areas of code that use that function know exactly how to unpack that array and how to use the values within them. As long as the Java code is untouched, it's guaranteed to work (because our system checked and built it), and Java would never run into NullPtrExceptions or anything else there. I imagine that we could similarly apply proofs to the size of input numbers to ensure that numeric overflows don't occur anywhere in the code, without writing "assertions" and "checks" everywhere, but restricting the allowed inputs through their types (dependent). Regarding DT PLs increasing precision, I completely agree. I think this expressivity is partially why I also felt like discussing DT PLs and Drasil in the same post. I believe the increased precisions assists the "staging" discipline significantly, assuming I'm understanding everything properly. I want to think about the questions you posed at the end (and the suitability for general programming question) more. In some sense, I almost want to say that it's wasteful (of the language features, not machine resources) to even use a DT PL to "directly" write general programs, and that we should be using DT PLs to write highly specific compilers that compiler specific kinds of programs directly for specific computer architectures. The information is exactly what compilers need to make optimizations on our programs anyways, no? |
Beta Was this translation helpful? Give feedback.
-
|
@smiths's post now had me thinking about this question: "And how much do we want our infrastructure to check for us?" Should we even want Drasil to check things for us, or should we require that users must provide proofs (through the type of their transcriptions) that their "stories" obey the rules of the stories (through type information)? I understand having Drasil, as a database of chunks, checking properties that all chunks must satisfy (ignoring their type, structure, data, etc.), such as checking that they are used in some way (either by reference in another chunk that satisfies this requirement, or is directly referenced in the main "story entry" of a Drasil program), but I wonder if the other checks can be moved to the type-checking time of a story, because all chunk types are "external" to Drasil, in the sense of Drasil that is a "database of chunks." |
Beta Was this translation helpful? Give feedback.
-
|
I like the idea of type-checking to put the onus on the user to provide a valid "story." If the input makes it through the type-checker, then the user will have increased confidence that they are doing things correctly. However, we'll want to have really good error messages, or the user won't know what they are doing wrong. 😄 We also have to be careful in all of this to not be too picky. In some cases a user might want to break some rules because their problem doesn't exactly fit our assumed use case. Since we don't have perfect knowledge of everything that Drasil could be used for, we want to allow flexibility. I don't know if it is an option for a type-checker to issue warnings, as opposed to errors, but some of our rules (at least initially) could be considered more guidelines than "laws." |
Beta Was this translation helpful? Give feedback.
-
|
I like it too. I vaguely imagine us allowing for type-hole programming (similar to "agda-mode") if we were to go down this route. I agree, overly restricting can be very problematic. I think this is also partially what @JacquesCarette meant by "When you're still exploring, they can be a funny game." However, it's largely based on the encoding of the "stories," so I think it's fair to say that the difficulty associated with using it is impacted by implementation. I think this goes back to #2896 (comment) (specifically, the last paragraph about validating domain models) in that the objectively "good story encoding" should be built with as much automated assistance as reasonably possible, but also that we stick to well-understood domains and a scientific audience that understands them. Though, with DTs, if I'm not mistaken, I think that we can still write the code as if it were simply typed as we would in Haskell (assuming the DT L admits the same "errors" and undefinedness). |
Beta Was this translation helpful? Give feedback.
-
|
Re: erasing proofs. This is done via the Manipulating syntax is indeed programming. Doing it in a way that you can reason about it involves logic. Re: tests vs proofs. What happens is that writing down a complete specification of what you want is extremely difficult. Some 'properties' are much easier to express using tests as a proxy. Re: "How much do we want our infrastructure to check for us?". Lots! But that doesn't mean that every check should result in an error (warnings are useful too). And it doesn't mean that all checks will be done using a single technology, or a single pass, or in a single Drasil component, or ... I think we need to start from a list of good properties of various artifacts (including cross-artifact properties), from which we can pick the "low hanging fruit". Often the simplest sanity checks are also surprisingly valuable. We don't really have a list of what makes a good story. We don't want complex properties - we don't want the users to give us "proofs". But we can ask users to to give us tidbits of evidence that justifies that their story is good. |
Beta Was this translation helpful? Give feedback.
-
|
Great conversation! I won't claim to understand all of it, but I think I get the gist. I especially like the last statement by Jason. The part about using DT PLs for specific problems, not for general programs. I'm sure there are much more complex examples, but the cases where I see DTs in our examples are for sequences of specific lengths. (At least I think this is an example of dependent types.) 😄 I'm pretty sure I saw other simple examples while thinking about how to add types to the SRS document. I'll watch for other examples and highlight them when they come up. @balacij if you see other examples of dependent types that could fit with our current examples, don't hesitate to point them out. I find I understand concepts better through examples, rather than abstract conversation. (Your Java Object[] example was easy to understand because you made it a specific example.) 😄 |
Beta Was this translation helpful? Give feedback.
-
|
Thank you! 😄 I think "Drasil might benefit from DTs" has been a re-occurring thought (at least for me), but I don't quite fully understand why I have this thought. I'll try to think of examples, but I think the increased precision that @JacquesCarette mentioned is the main feature it has over Haskell. The discussion in 760 was an interesting spark to this post. |
Beta Was this translation helpful? Give feedback.
-
|
Drasil can benefit from the ideas of dependent types, without using them directly. We do use a lot of staging already, and we can get many of the benefits of dependent types through doing generation-time checks. We are nowhere near exhausting that way of doing things, so we should fully mine that first. |
Beta Was this translation helpful? Give feedback.
-
|
I like the idea of having examples of the things we want to do that may or may not require DTs. When we have an example of something we want to accomplish, we can then figure out the best way to do it. 😄 |
Beta Was this translation helpful? Give feedback.
-
In CAS 760, we discussed type systems and some of the common ones. In particular, we discussed the original type system that Russell discussed, improved systems, such as Churchs, Henkins, and Martin-Lofs. Dr Farmer noted that he's still skeptical of dependently typed systems (in particular in their usage for general programs), and is waiting for more research on the topic. In class, he noted two (2) main issues he has with it: (i) runtime performance, and (ii) lack of producing classical theorem proofs (i.e., there are certain theorems that we don't have any proofs for [and/or proofs are unlikely/impossible to be found], such as the proof of, I believe,
p \lor \lnot p).Let's unpack these arguments a bit more: Regarding (i), runtime performance is impacted due to the overhead of needing to provide explicit "proofs" (witnesses) everywhere, and the overhead of using inefficient data structures to contain data. Regarding (ii), the issue focuses on discussing how the things we can say in the language is limited.
I completely agree with these issues and perhaps even the consequence, but I'm hesitant to leave the consequence as it is.
Regarding (i), the information is still important to us to ensure the artifacts are "high quality" (in terms of reliability and safety). The "type safety" obtained is not something we want to fully lose at runtime. It is perhaps something that can be removed from "explicit" witnesses and made "implicit" through "insider knowledge." The type information is very helpful at the programming/development stage to ensure that the software does as it is intended, but perhaps not as useful in the usage stage. For example, programming with your programs partially interpreted and evaluated before compilation (such as in Agda) speeds up the development process considerably. Additionally, needing nearly zero (0) unit tests (because you have proofs instead) is also something that benefits the programmer. Going the complete opposite direction (going fully back into manually writing Java + unit tests seems wasteful of the information). Regarding (ii), I'm hesitant to agree that the issue of inexpressibility would appear so often in dependently typed programming languages that they would be unusable, primarily because we can just default to using "simple"-style programs written with a dependently typed programming languages wherever it fails.
However, both issues assume that the desired programs should be written directly in a dependently typed language and processed using its compiled form.
Enter Drasil. Was it obvious I was going to bring this back to Drasil?
With Drasil, we focus on generating software artifacts as a side effect of strong (large depth + wide breadth) knowledge capture. Now, we can try to naively convert our Haskell code into Agda (a dependently typed programming language), and, other than our TTF encodings, it should be a fairly straight forward translation (Note: I am not saying we should do this, just imagining it). In this case, we would be programming specific kinds of with a dependently typed programming language, but we would be directing what the target artifacts do (directly) through "generating them" ourselves rather than using the general translation of Drasil into a program. There are benefits to switching Drasil to a dependently typed programming language (potentially such as in #2181).
So, I think we can refine the consequence of the two (2) issues: Dependently typed programming languages are poor languages for directly writing efficient & performant software. However, they are suitable languages for describing general software (and knowledge), generating efficient and performance software, and even automatically maintaining them. Drasil would obtain the Curry-Howard Correspondence and we might be able to provide proofs that artifacts conform to specifications in one way or another. By using the "witnesses/proofs" in the artifact generation step, we can implicitly assume a lot of information based on them through the generated software artifacts (and potentially even in areas where we might want dependent types in the host language of an artifact, such as in the case of array lengths).
Regarding (i), we would eliminate the runtime cost, and move it to the development time. However, this might become a net "benefit" because it assists in the development of software (for example, type-hole programming can be something used to develop our programs, and prove properties about systems). Regarding (ii), since we stick to the walls of "well-understood" knowledge, we shouldn't have issues with expressibility of knowledge, but, when we do have issues with "proving" things at least, we should be able to "postulate" them (as done in Agda), and provide explicit proofs outside of the program (classically).
Ultimately, I think I agree with Dr. Farmers statement that they might not be suitable for general-purpose programming (at least not for many applications yet), but I think we can refine the position to discuss what it might be good at -- namely, generating safe and reliable programs, similar to what we're doing with Haskell and Drasil.
Of course, I could be off in this, but I believe there's at least a discussion to be had. This also relates to Chapter 2 of my thesis, the idealized development workflow, and PhD topic #3003.
ASIDE NOTE (A): Assuming I were to suggest we re-write Drasil, instead of suggesting re-writing Drasil in Agda (or any other language), I would probably first consider we make Drasil itself some kind of dependently typed programming language (but likely one that wouldn't necessarily 'compile' down to a runnable executable, but a dependently typed interpreted programming language). Think of this idea as some sort of PL as how Elm is to functional programming. The Elm program itself is built around a specific "MVU" structure, and Drasil is similar in that it's around a "Story to Artifact" structure.
ASIDE NOTE (B): Assuming ASIDE NOTE (A) makes sense, I think Drasil would be some sort of poster child project for dependent type systems (and maybe for Haskell and STT too).
This "discussion" ticket is really just that -- a discussion. I'm just curious about what others think about the issues with dependently typed programming languages, in particular in the context of Drasil, because I think "Drasils ideology" might be a suitable scheme for developers to write usable software using a dependently typed programming language.
Beta Was this translation helpful? Give feedback.
All reactions