10 ms·

A dependently typed language for proofs that you can implement in one day

134 points by caotic123 5y ago

cjfd 5y ago
What exactly are the foundations of this? The rules on the page suggest that it is basically the calculus of constructions but the example involving the list suggests that there are inductive types too. Are the inductive types part of the foundations and omitted in the list of rules or are they something else that is not part of the foundation?
- caotic123 5y ago
  Pompom does not offer inductive data types, instead, it provides static symbols (as in the LF framework or λΠ-Calculus Modulo). Of course, we do not use the rewriting foundation of these frameworks, however, we apply a usual unification algorithm to get the same power. There are a lot of things that need proper formalization in the core, but the intention of this work is not it yet. To be fair, not inductive data types as Coq/Agda.
  - deleted 5y ago
    [deleted]
jimsimmons 5y ago
I’m constantly baffled by what functional programmers call “simple”. I’m sure this language does a lot with little but calling it simple is audacious to say the least. Why do so many things happen in a single line? Lack of imperative constructs in these languages forces one to nest a lot to be expressive and we get a symbol salad. It’s almost as if the code got passed through a minifier/function inliner. Unless FP embraces more modular and structured ways of programming it’ll always remain a niche. OCaml’s ‘let’ and Haskell’s ‘where’ are steps in the right direction but we need to go a lot farther. To think that any human, with any amount of training, can parse such code in one pass is a fantasy. Since parsing is part of the coding loop, developer productivity is compromised massively. Mathematics has a similar problem where single letter variable names with tiny letters on all 4 corners are ubiquitously used. There’s definitely a tendency in the community to play “symbol” golf. It’s high time we improve ergonomics of both math and FP because the rewards can be tremendous. Rust manages to do some of this to great success and programmers have embraced it so well.
- tome 5y ago
  > I’m constantly baffled by what functional programmers call “simple”. This github repo is clearly not for "functional programmers" nor a generalist audience on HN. It's for experts in type theory, graduate students, academics etc.. The word "simple" is relative to that particular audience.
  - jimsimmons 5y ago
    Posting to HN with a title that says “you can” makes your point moot no?
    - tome 5y ago
      Hmmm yes perhaps. Imagine a submission titled "A linear filter for DSP you can solder up yourself in a day". 95% on HN couldn't. Would the response "I’m constantly baffled by what electrical engineers call “simple”." be warranted? Maybe.
    - gpderetta 5y ago
      As someone that has very little idea of what all of that is, I think the title is great and certainly made me consider looking into the implementation. It might be wildly optimistic, but encouraging people to learn new things, especially by trying, is always a good thing.
      - caotic123 5y ago
        Thank you, it is exactly what I was expecting people to understand!
    - Zababa 5y ago
      I think that's the case for most DIY projects that we have on Hacker News. Most assume that you have lots of X in the first place. It can be lots of experience with programming languages, it can be a lot of space, it can be tools.
- caotic123 5y ago
Twirrim 5y ago
> Pompom language is so simple that you can implement it yourself just by looking in the source code (you can think that our language is the BASIC language of proof assistants). List | A :: ~ * ~> * => {(list A) :: |new |empty }. // A list is either a new or a empty constructor Okay... BASIC is a high level language, and it's aimed at people who are not involved in sciences. If your goal is to have a high level syntax, and aiming it at people maybe outside of those with formal proof background, I think that's a big miss. The syntax is anything but BASIC, compounded by the choice of lisp.
- tluyben2 5y ago
  > the choice of lisp. Where? No lisp here as far as I can see. Haskell you mean? But this is BASIC and simple to follow (including the source code of the language) for people interested in type systems and languages, not for just anyway. If you scroll down you see then the calculus with the words simple as well. This means: for people interested in implementing this, it is a very simple implementation and that is correct indeed. Nice work!
- caotic123 5y ago
  I think you misunderstood, I have just made an analogy with BASiC. BASIC is normally a language that students used to implement when they are dealing with compiler topics. The fact is because BASIC is simple to learn and implement in the universe of structural languages. So, what I am saying is that you can do the same thing with Pompom, but of course, aiming at people that have at least a little experience with functional programming and type systems.
  - tluyben2 5y ago
    It is nicely done; the implementation is indeed simple and easy to read! It hopefully will make more language implementors understand. I guess comparing it to BASIC is not good as this is complex matter: languages like Idris that have a vastly more complex implementation but therefore also a nice (imho) syntax, are still hard for most without theoretical background (I was raised and educated by Dijkstra pupils so it was pounded into me from very young); I found The Little Typer a good read on the subject, but that might be impossible for people without background as well; I cannot really estimate that.
choeger 5y ago
The syntax is quite ... complex, I dare say. It looks like you borrowed from Haskell, which already makes it hard to gain an intuitive understanding of the syntax and added bars?
isaac21259 5y ago
Sorry but you cannot implement this in a day. I've written my own language very similar to this and from my experience it takes way longer. Implementing type checking for just lambdas, pi types, universes, unit, and absurd would take a day or two on it's own. Not to mention Sigma types, co-product types, w-types, identity types, natural numbers, and lists. You also have type inference and evaluation. Also the time spent coming to grips with what all of this means. It's a really cool project but I expect it would take a week minimum to implement this and have a solid understanding of everything you've done.
- caotic123 5y ago
  Well, half of it does not have to be necessarily implemented in the core (we are not talking of complex languages like Agda), but yeah, I think if you do not know anything about the PomPom will take some time to finalize it. But I am pretty sure if you have some knowledge about the core you can have a lot of progress in one day.
- igravious 5y ago
  A week minimum? This is such a frustrating space. The bar for understanding this code and toy project code like this (in this space) is in-depth knowledge of either ML or Haskell (or some functional language with proper built-in functions but generally either ML or Haskell†) … this is key; all these type-theoretic "look at what I built" jaunts leverage these languages. In this case PomPom says: "The only requisite is cabal and GHC" – which is nothing at all like saying that all you need is C and its standard library. How long would it take you to write your dependently typed language PomPom in C with just its standard library? If the answer to this is far more than a day then I guess that Cabal (I would capitalise Cabal) and GHC are doing some pretty heavy lifting. I don't think this is me being petty. Why is Cabal needed. Because from looking at the code, at least the parser Parsec. Oh. Ok. Why not say Parsec is needed? It would be weird for me to say that a language I wrote only needed Ruby and Bundler/Rubygems … I mean what would that even mean? Most everybody else writes "The only requisite is cabal and GHC" as I wrote PomPom in the GHC version of Haskell, you need at least version X.Y.Z of GHC and it relies on the following language features (a,b,c,…)‡ and the following external libraries (A,B,C,…). So you've written a whole language and, get this, there are no comments in the code about the language syntax and the README jumps straight to "For example proving that inserting a element in any position in a list always returns a non-empty list can be encoded like :" I mean … No, here is the syntax of PomPom. Why? I can only conclude that the syntax does not matter. And isn't it an odd and strange language where the syntax is unimportant? > Sorry but you cannot implement this in a day. You're absolutely correct you can't. First of all you need a deep understanding off GHC and its ecosystem. Second of all you need a good grasp of type theory. Then you'd have to figure out the syntax off PomPom, then you'd have to reimplement all the important parsing and type checking bits. Now say that you wanted to use the esoteric C or one of its super esoteric descendents (C#, Java, C++, Kotlin, Swift, etc.) or you wanted to use something exotic like Rust or Go or even one of those dynamic languages that nobody uses (Javascript, Python, Ruby, etc.) because you didn't feel like learning GHC and its ecosystem. What then? What I'm trying to get at is that I would respond to the claims in this space that you can build language CoolTypes in X days with a roll of the eyes, or more charitably a raised eyebrow (would respond witth something going on round the ocular area is what I'm getting at). † Not to mention Coq, or Idris, or LEAN, Agda, or god knows what else ‡ We all know that it's never just GHC, it's always at least version X.Y.Z of GHC with experimental(?) language features a and b and so on enabled.
dwohnitmok 5y ago
I find the often ML-inspired syntax too high of a bar for most programmers to clear when being introduced to a language. I think a syntax more similar to something like what is introduced here: https://shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html https://shuangrimu.com/posts/language-agnostic-intro-to-depe... more accessible for a lot of programmers. I separately think that proofs are actually a bit overblown when it comes to dependent types and that dependent types are most useful for specification, but often times could benefit from "fake" implementations.
- caotic123 5y ago
  The syntax you presented is really very accessible. Of course, it makes things a little more verbose, but I think you are right, the path for bringing more attention to dependent types is probably making more accessible also. Btw, great article I will have a more detailed look after.
  - dwohnitmok 5y ago
    That syntax might be unacceptably verbose with too many usually implicit arguments. However, I also think that implicit arguments primarily are needed when working with heavily-dependently-typed data structures, which I think is a bad way of working with dependent types (e.g. I don't like length indexed vectors). Instead if you primarily work with non-dependent data structures and then pass in dependently-typed invariants as a separate argument, you can avoid a lot of the complexity associated with dependent types. This allows your dependently typed arguments to not have a runtime representation, e.g. they could be given zero multiplicity in Idris. This in turn allows you to easily substitute a property test or an external solver (or just a human "trust me" override) instead of being forced to always prove everything since you no longer require a true implementation of a dependent type. This in turn simultaneously severely reduces the need for elaborate implicit arguments and makes verbosity much easier to deal with.
    - arianvanp 5y ago
      This sounds interesting. Can you give a concrete example? This seems to really fall into place with my feeling that heavily dependently typed data types Ans programs using them are hard to refactor as the invariants that you break in the refactor cascade through your entire program. Separating them probably makes life easier
NancyFXTrade 5y ago
Hi, I am Nancy robert, a professional bitcoin miner and forex trader, i can assist you on how to make money online by getting involved with a high profitable business (Forex, Binary Options, Bitcoin Mining ). Make huge profits weekly from your initial investment. Do you know with my trading software and signals you can make a good profit weekly if you invest with minimum of: INVEST $500 GET $6000 INVEST $1500 GET $15,000 INVEST $3000 GET $30,000 INVEST $4000 GET $40,000 INVEST $5000 GET $50,000 But the major condition here, is that at the end of every trading session, after successful withdrawal, we will have 20% of profit made, leaving you with 80%. This forex trading is helping the life's of me and my investors. Get started today with trading and earn a living. Work from anywhere and monitor your trade with your phone or computer. Kindly reply me if interested or contact me on whatsapp +13198204277 or Email:nancyrobertcryptoxpert@aol.com No risk involved 100% safe.
baddash 5y ago
So, as someone who is curious but have no idea of the theoretical background here.. what should I learn in order to help me understand the code + use this language in a basic way? I think the idea of being able to construct proofs is pretty cool but I'm pretty lost here.
- evolveyourmind 5y ago
  If you want to learn more about the basics of theorem proving through dependent types, Wadler’s Agda tutorial at https://plfa.github.io https://plfa.github.io would be a good starting point
  - baddash 5y ago
    appreciate it, thanks
- caotic123 5y ago
  I also recommend the software foundations in coq https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/.
anfelor 5y ago
The Readme defines: // Data NonEmpty = | New a (NonEmpty a) NonEmpty |A :: ~ * ~> * => {(list A) :: |new}. // A list non-empty is list only with new constructor The haskell datatype reads like a co-inductive definition: a stream of list elements. But the NonEmpty in your language should be data NonEmpty = New a (List a) right?
- caotic123 5y ago
  Exactly, it does not necessarily means co-data, thank you for reporting it, i will fix it.
bsaul 5y ago
in practice, what kind of proof are people building when building real world programs ? Are people writing only top level assertion ( such as "this main function always terminate") and the checker points at all the gaps ? Or does one has to write proofs for every single intermediate layer and functions ? In wich case, do people then have access to prebuilt "proven functions" in a stdlib ? such as "NeverEmptyList" or "AlwaysGreaterThanXVariable" ?
- jacobparker 5y ago
  Some examples from a Software Foundations (a series of books about Coq, available online): I just wrote something I called insertion sort. I want to know that this is a valid implementation of sorting. What does it mean to be a sorting algorithm? It means that the output is sorted, and it's a permutation (shuffling) of the input. This is an exercise here: https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.html https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.h... Say I've written a Red-Black tree. I want to know that it behaves like a map, or that it keeps the tree appropriately balanced (which is related to performance): https://softwarefoundations.cis.upenn.edu/vfa-current/Redblack.html https://softwarefoundations.cis.upenn.edu/vfa-current/Redbla... One more: say you have specified a programming language, which includes describing the structure of programs (the grammar essentially) and "small step" semantics (e.g `if true then x else y` can take a step to `x`). It would be interesting to show that any well-typed halting program can be evaluated in multiple steps to exactly one value (i.e. the language is deterministic and "doesn't get stuck" (or, in a sense, have undefined behaviour)). That's the subject of volume 2 https://softwarefoundations.cis.upenn.edu/plf-current/toc.html https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht... Beyond this, you may have done a similar thing for a lower level language (machine assembly, wasm, ...) and have a compiler from your language to the low level language. You may want to prove that the compiler "preserves" something, e.g. the compiled output evaluates to the same result ultimately. RE: termination, in something like Coq that is a bit special because every function terminates by construction. That might sound limiting but it's not really/there are ways around it. It would, however, be impossible to write something like the Collatz function in Coq and extract it in the obvious sense. EDIT: and there are other ways these tools can (theoretically) be used to work with programs, but that's a long story. There have been real-world programs built like this, but it is very uncommon at this time. It is an area of active research.
mbid 5y ago
>Pompom is an attractive implementation of an extensional (!) dependently typed language >Pompom provides [...] a strong normalization system How is this possible? Extensional dependent type theory has undecidable term/type equality, so there cannot be a strong normalization algorithm.
- caotic123 5y ago
  Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).
  - caotic123 5y ago
    As far i know, pompom has a decidable type check though.
imode 5y ago
This isn't a one-day implementation.
mbrodersen 5y ago
The syntax is really bad. And I am familiar with Haskell, Lean, Idris, Agda etc. If the author reads this, I recommend instead copying the syntax used by Lean, Idris, or Agda. They are very close to each other and all good.
- caotic123 5y ago
  The syntax is also a point of "easy for parse", for sure it can be improved but IDK if just copying the syntax of these languages is the better solution.

134 points by caotic123 5y ago

cjfd 5y ago

What exactly are the foundations of this? The rules on the page suggest that it is basically the calculus of constructions but the example involving the list suggests that there are inductive types too. Are the inductive types part of the foundations and omitted in the list of rules or are they something else that is not part of the foundation?

caotic123 5y ago
Pompom does not offer inductive data types, instead, it provides static symbols (as in the LF framework or λΠ-Calculus Modulo). Of course, we do not use the rewriting foundation of these frameworks, however, we apply a usual unification algorithm to get the same power. There are a lot of things that need proper formalization in the core, but the intention of this work is not it yet. To be fair, not inductive data types as Coq/Agda.
- deleted 5y ago
  [deleted]

jimsimmons 5y ago

I’m constantly baffled by what functional programmers call “simple”. I’m sure this language does a lot with little but calling it simple is audacious to say the least. Why do so many things happen in a single line? Lack of imperative constructs in these languages forces one to nest a lot to be expressive and we get a symbol salad. It’s almost as if the code got passed through a minifier/function inliner. Unless FP embraces more modular and structured ways of programming it’ll always remain a niche. OCaml’s ‘let’ and Haskell’s ‘where’ are steps in the right direction but we need to go a lot farther. To think that any human, with any amount of training, can parse such code in one pass is a fantasy. Since parsing is part of the coding loop, developer productivity is compromised massively. Mathematics has a similar problem where single letter variable names with tiny letters on all 4 corners are ubiquitously used. There’s definitely a tendency in the community to play “symbol” golf. It’s high time we improve ergonomics of both math and FP because the rewards can be tremendous. Rust manages to do some of this to great success and programmers have embraced it so well.

tome 5y ago
> I’m constantly baffled by what functional programmers call “simple”. This github repo is clearly not for "functional programmers" nor a generalist audience on HN. It's for experts in type theory, graduate students, academics etc.. The word "simple" is relative to that particular audience.
- jimsimmons 5y ago
  Posting to HN with a title that says “you can” makes your point moot no?
  - tome 5y ago
    Hmmm yes perhaps. Imagine a submission titled "A linear filter for DSP you can solder up yourself in a day". 95% on HN couldn't. Would the response "I’m constantly baffled by what electrical engineers call “simple”." be warranted? Maybe.
  - gpderetta 5y ago
    As someone that has very little idea of what all of that is, I think the title is great and certainly made me consider looking into the implementation. It might be wildly optimistic, but encouraging people to learn new things, especially by trying, is always a good thing.
    - caotic123 5y ago
      Thank you, it is exactly what I was expecting people to understand!
  - Zababa 5y ago
    I think that's the case for most DIY projects that we have on Hacker News. Most assume that you have lots of X in the first place. It can be lots of experience with programming languages, it can be a lot of space, it can be tools.
caotic123 5y ago

Twirrim 5y ago

> Pompom language is so simple that you can implement it yourself just by looking in the source code (you can think that our language is the BASIC language of proof assistants). List | A :: ~ * ~> * => {(list A) :: |new |empty }. // A list is either a new or a empty constructor Okay... BASIC is a high level language, and it's aimed at people who are not involved in sciences. If your goal is to have a high level syntax, and aiming it at people maybe outside of those with formal proof background, I think that's a big miss. The syntax is anything but BASIC, compounded by the choice of lisp.

tluyben2 5y ago
> the choice of lisp. Where? No lisp here as far as I can see. Haskell you mean? But this is BASIC and simple to follow (including the source code of the language) for people interested in type systems and languages, not for just anyway. If you scroll down you see then the calculus with the words simple as well. This means: for people interested in implementing this, it is a very simple implementation and that is correct indeed. Nice work!
caotic123 5y ago
I think you misunderstood, I have just made an analogy with BASiC. BASIC is normally a language that students used to implement when they are dealing with compiler topics. The fact is because BASIC is simple to learn and implement in the universe of structural languages. So, what I am saying is that you can do the same thing with Pompom, but of course, aiming at people that have at least a little experience with functional programming and type systems.
- tluyben2 5y ago
  It is nicely done; the implementation is indeed simple and easy to read! It hopefully will make more language implementors understand. I guess comparing it to BASIC is not good as this is complex matter: languages like Idris that have a vastly more complex implementation but therefore also a nice (imho) syntax, are still hard for most without theoretical background (I was raised and educated by Dijkstra pupils so it was pounded into me from very young); I found The Little Typer a good read on the subject, but that might be impossible for people without background as well; I cannot really estimate that.

choeger 5y ago

The syntax is quite ... complex, I dare say. It looks like you borrowed from Haskell, which already makes it hard to gain an intuitive understanding of the syntax and added bars?

isaac21259 5y ago

Sorry but you cannot implement this in a day. I've written my own language very similar to this and from my experience it takes way longer. Implementing type checking for just lambdas, pi types, universes, unit, and absurd would take a day or two on it's own. Not to mention Sigma types, co-product types, w-types, identity types, natural numbers, and lists. You also have type inference and evaluation. Also the time spent coming to grips with what all of this means. It's a really cool project but I expect it would take a week minimum to implement this and have a solid understanding of everything you've done.

caotic123 5y ago
Well, half of it does not have to be necessarily implemented in the core (we are not talking of complex languages like Agda), but yeah, I think if you do not know anything about the PomPom will take some time to finalize it. But I am pretty sure if you have some knowledge about the core you can have a lot of progress in one day.
igravious 5y ago
A week minimum? This is such a frustrating space. The bar for understanding this code and toy project code like this (in this space) is in-depth knowledge of either ML or Haskell (or some functional language with proper built-in functions but generally either ML or Haskell†) … this is key; all these type-theoretic "look at what I built" jaunts leverage these languages. In this case PomPom says: "The only requisite is cabal and GHC" – which is nothing at all like saying that all you need is C and its standard library. How long would it take you to write your dependently typed language PomPom in C with just its standard library? If the answer to this is far more than a day then I guess that Cabal (I would capitalise Cabal) and GHC are doing some pretty heavy lifting. I don't think this is me being petty. Why is Cabal needed. Because from looking at the code, at least the parser Parsec. Oh. Ok. Why not say Parsec is needed? It would be weird for me to say that a language I wrote only needed Ruby and Bundler/Rubygems … I mean what would that even mean? Most everybody else writes "The only requisite is cabal and GHC" as I wrote PomPom in the GHC version of Haskell, you need at least version X.Y.Z of GHC and it relies on the following language features (a,b,c,…)‡ and the following external libraries (A,B,C,…). So you've written a whole language and, get this, there are no comments in the code about the language syntax and the README jumps straight to "For example proving that inserting a element in any position in a list always returns a non-empty list can be encoded like :" I mean … No, here is the syntax of PomPom. Why? I can only conclude that the syntax does not matter. And isn't it an odd and strange language where the syntax is unimportant? > Sorry but you cannot implement this in a day. You're absolutely correct you can't. First of all you need a deep understanding off GHC and its ecosystem. Second of all you need a good grasp of type theory. Then you'd have to figure out the syntax off PomPom, then you'd have to reimplement all the important parsing and type checking bits. Now say that you wanted to use the esoteric C or one of its super esoteric descendents (C#, Java, C++, Kotlin, Swift, etc.) or you wanted to use something exotic like Rust or Go or even one of those dynamic languages that nobody uses (Javascript, Python, Ruby, etc.) because you didn't feel like learning GHC and its ecosystem. What then? What I'm trying to get at is that I would respond to the claims in this space that you can build language CoolTypes in X days with a roll of the eyes, or more charitably a raised eyebrow (would respond witth something going on round the ocular area is what I'm getting at). † Not to mention Coq, or Idris, or LEAN, Agda, or god knows what else ‡ We all know that it's never just GHC, it's always at least version X.Y.Z of GHC with experimental(?) language features a and b and so on enabled.

dwohnitmok 5y ago

I find the often ML-inspired syntax too high of a bar for most programmers to clear when being introduced to a language. I think a syntax more similar to something like what is introduced here: https://shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html https://shuangrimu.com/posts/language-agnostic-intro-to-depe... more accessible for a lot of programmers. I separately think that proofs are actually a bit overblown when it comes to dependent types and that dependent types are most useful for specification, but often times could benefit from "fake" implementations.

caotic123 5y ago
The syntax you presented is really very accessible. Of course, it makes things a little more verbose, but I think you are right, the path for bringing more attention to dependent types is probably making more accessible also. Btw, great article I will have a more detailed look after.
- dwohnitmok 5y ago
  That syntax might be unacceptably verbose with too many usually implicit arguments. However, I also think that implicit arguments primarily are needed when working with heavily-dependently-typed data structures, which I think is a bad way of working with dependent types (e.g. I don't like length indexed vectors). Instead if you primarily work with non-dependent data structures and then pass in dependently-typed invariants as a separate argument, you can avoid a lot of the complexity associated with dependent types. This allows your dependently typed arguments to not have a runtime representation, e.g. they could be given zero multiplicity in Idris. This in turn allows you to easily substitute a property test or an external solver (or just a human "trust me" override) instead of being forced to always prove everything since you no longer require a true implementation of a dependent type. This in turn simultaneously severely reduces the need for elaborate implicit arguments and makes verbosity much easier to deal with.
  - arianvanp 5y ago
    This sounds interesting. Can you give a concrete example? This seems to really fall into place with my feeling that heavily dependently typed data types Ans programs using them are hard to refactor as the invariants that you break in the refactor cascade through your entire program. Separating them probably makes life easier

NancyFXTrade 5y ago

Hi, I am Nancy robert, a professional bitcoin miner and forex trader, i can assist you on how to make money online by getting involved with a high profitable business (Forex, Binary Options, Bitcoin Mining ). Make huge profits weekly from your initial investment. Do you know with my trading software and signals you can make a good profit weekly if you invest with minimum of: INVEST $500 GET $6000 INVEST $1500 GET $15,000 INVEST $3000 GET $30,000 INVEST $4000 GET $40,000 INVEST $5000 GET $50,000 But the major condition here, is that at the end of every trading session, after successful withdrawal, we will have 20% of profit made, leaving you with 80%. This forex trading is helping the life's of me and my investors. Get started today with trading and earn a living. Work from anywhere and monitor your trade with your phone or computer. Kindly reply me if interested or contact me on whatsapp +13198204277 or Email:nancyrobertcryptoxpert@aol.com No risk involved 100% safe.

baddash 5y ago

So, as someone who is curious but have no idea of the theoretical background here.. what should I learn in order to help me understand the code + use this language in a basic way? I think the idea of being able to construct proofs is pretty cool but I'm pretty lost here.

evolveyourmind 5y ago
If you want to learn more about the basics of theorem proving through dependent types, Wadler’s Agda tutorial at https://plfa.github.io https://plfa.github.io would be a good starting point
- baddash 5y ago
  appreciate it, thanks
caotic123 5y ago
I also recommend the software foundations in coq https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/.

anfelor 5y ago

The Readme defines: // Data NonEmpty = | New a (NonEmpty a) NonEmpty |A :: ~ * ~> * => {(list A) :: |new}. // A list non-empty is list only with new constructor The haskell datatype reads like a co-inductive definition: a stream of list elements. But the NonEmpty in your language should be data NonEmpty = New a (List a) right?

caotic123 5y ago
Exactly, it does not necessarily means co-data, thank you for reporting it, i will fix it.

bsaul 5y ago

in practice, what kind of proof are people building when building real world programs ? Are people writing only top level assertion ( such as "this main function always terminate") and the checker points at all the gaps ? Or does one has to write proofs for every single intermediate layer and functions ? In wich case, do people then have access to prebuilt "proven functions" in a stdlib ? such as "NeverEmptyList" or "AlwaysGreaterThanXVariable" ?

jacobparker 5y ago
Some examples from a Software Foundations (a series of books about Coq, available online): I just wrote something I called insertion sort. I want to know that this is a valid implementation of sorting. What does it mean to be a sorting algorithm? It means that the output is sorted, and it's a permutation (shuffling) of the input. This is an exercise here: https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.html https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.h... Say I've written a Red-Black tree. I want to know that it behaves like a map, or that it keeps the tree appropriately balanced (which is related to performance): https://softwarefoundations.cis.upenn.edu/vfa-current/Redblack.html https://softwarefoundations.cis.upenn.edu/vfa-current/Redbla... One more: say you have specified a programming language, which includes describing the structure of programs (the grammar essentially) and "small step" semantics (e.g `if true then x else y` can take a step to `x`). It would be interesting to show that any well-typed halting program can be evaluated in multiple steps to exactly one value (i.e. the language is deterministic and "doesn't get stuck" (or, in a sense, have undefined behaviour)). That's the subject of volume 2 https://softwarefoundations.cis.upenn.edu/plf-current/toc.html https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht... Beyond this, you may have done a similar thing for a lower level language (machine assembly, wasm, ...) and have a compiler from your language to the low level language. You may want to prove that the compiler "preserves" something, e.g. the compiled output evaluates to the same result ultimately. RE: termination, in something like Coq that is a bit special because every function terminates by construction. That might sound limiting but it's not really/there are ways around it. It would, however, be impossible to write something like the Collatz function in Coq and extract it in the obvious sense. EDIT: and there are other ways these tools can (theoretically) be used to work with programs, but that's a long story. There have been real-world programs built like this, but it is very uncommon at this time. It is an area of active research.

mbid 5y ago

>Pompom is an attractive implementation of an extensional (!) dependently typed language >Pompom provides [...] a strong normalization system How is this possible? Extensional dependent type theory has undecidable term/type equality, so there cannot be a strong normalization algorithm.

caotic123 5y ago
Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).
- caotic123 5y ago
  As far i know, pompom has a decidable type check though.

imode 5y ago

This isn't a one-day implementation.

mbrodersen 5y ago

The syntax is really bad. And I am familiar with Haskell, Lean, Idris, Agda etc. If the author reads this, I recommend instead copying the syntax used by Lean, Idris, or Agda. They are very close to each other and all good.

caotic123 5y ago
The syntax is also a point of "easy for parse", for sure it can be improved but IDK if just copying the syntax of these languages is the better solution.