2
$\begingroup$

I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is:

  • Consistent/Normalizing

  • Can express all the type families from Coq (or even Agda)

  • Allows for a simple expression of recursion over these families

  • Simple or has a small number of core constructions (Π,Σ,μΠ,Σ,μ).

Now, suppose we take the elementary affine logic and extend it with dependent types and fix. It is easy to prove that language is consistent and normalizing as a consequence of EAL. It can, I believe, express all the type families from Coq, with lambda-encodings and since it has fix. A simple expression of recursive algorithms is possible with church-encodings for iteration and scott-encodings for matching. And it is obviously simple, as it only has , ! and let. Moreover, such language would have the very comforting property that it can be reduced optimally using the abstract fragment of Lamping's algorithm.

All things considered, such language looks like a perfect candidate for the role of a small functional core that serves as an universal code-interchange format, as proposed by Gabriel. Is my suspicion correct, or is there any problem with this reasoning?

$\endgroup$
  • 1
    $\begingroup$ Is it actually easy to prove that the language is consistent and normalizing? $\endgroup$ – cody Jul 26 '17 at 17:40
  • $\begingroup$ @cody is that a rhetorical question? I'm not sure, but I took that info from this answer: cstheory.stackexchange.com/questions/36767/… $\endgroup$ – MaiaVictor Jul 26 '17 at 17:46
  • $\begingroup$ @cody note that I don't agree with Damiano's point that it'd not be natural. It'd be just different. You can use the Scott-Encoding for pattern matching terms that you don't know the length, and the Church-Encoding to express recursive algorithms naturally. A combination of both would allow you to express many things in very simple manners. $\endgroup$ – MaiaVictor Jul 26 '17 at 17:48
  • $\begingroup$ The question was not rhetorical, I understand better thanks to your reference. $\endgroup$ – cody Jul 26 '17 at 18:23
  • $\begingroup$ I read some of your thoughts bout Scott encoding on Morte and the type for natural numbers you propose is Nat = fix self . (Nat : *) -> (self -> Nat) -> Nat -> Nat. While this encoding captures pattern matching, it doesn't capture recursion. To allow recursion with pattern matching you need term level fixed points or a more complex machinery (mutually recursive definitions) as the paper on self types says. $\endgroup$ – user3368561 Jul 11 '18 at 17:44
2
$\begingroup$

This is a tough question to answer, since simplicity is in the eye of the beholder.

Certainly $\lambda$-encodings have their drawbacks, there are reasons why Coq decided to move away from them, the most obvious one is the inability to introspect the subterms during recursion. The second is the general awkwardness in defining deeply or mutually recursive functions.

As you note, the "fix-encoding" avoids this but then it is hard to define non-constant functions (which is the point Damiano brings up)! You have to choose: introspection or recursion. Often we want both.

I'm also a bit skeptical of Gabriel's proposal: how does he compute exponentials on "native" ints without recursion?

In addition, the fact that EAL can only express elementary functions seems intuitively like it should restrict "natural" ways of writing recursions. In particular this shouldn't be well-defined:

Fixpoint acker m := match m with | O => S | S m => (fix acker' f n := match n with | O => f 1 | S n => f (acker' f n) end) (acker m) end.

since it defines a non-elementary function. So what feature of EAL is preventing this definition? If I understand correctly (and I'm not sure I do), the term f (acker' f n) cannot be well-typed, there must be some "stratum" which prevents the final application of f.

So certainly the natural way to write this function is forbidden. What other natural things are forbidden in this framework? It's hard to say without asking a specialist, but my guess is that there will be a fair number of things. Linear type systems can be powerful frameworks, but they aren't very convenient or natural for writing programs.

It's also an important fact (but maybe this is asking for a lot) that $0\neq 1$ is directly provable in Coq, thanks to large elimination. Is adding this feature easy in your proposal?

Finally, there's something I'm always worried about when I hear about type systems with linear logic: how hard is it to write a type checker? Certainly the checker has to figure out which pieces of the context go where when performing checking. Also the user or the front-end has to figure out where to put all the !s, if you want to have any non-linear components (and you usually do!).

To summarize, my answer to the question "is EAL with dependent types simple, consistent and expressive?" is probably not: it is probably consistent, but I'm not sure it's simple, and I don't think it is sufficiently expressive.

However, there is a "simple" way to refute this claim: write down the system definition, ideally prove it consistent, and write down some simple functions using it, probably up to, say, red-black trees or something. If the fully detailed syntax and typing rules is large, then the system is complex, if it is very tough to write down the functions, then it is insufficiently expressive. If it is neither of those, then you've answered a tough open problem in type theory!

$\endgroup$
  • $\begingroup$ Amazing answer, thank you! So, I guess you're fairly sure that if I follow your challenge I'll end up with either complex typing rules or an inexpressive system, but still think it is worth trying nether less if only for the learning opportunity, right? $\endgroup$ – MaiaVictor Jul 26 '17 at 18:33
  • $\begingroup$ Absolutely! In addition, even if the system ends up being complex and hard to work with, I think there is legitimate interest in understanding how to work with it, from the point of view of programing (linear types as resource) as well as logic (reverse mathematics and such). $\endgroup$ – cody Jul 26 '17 at 20:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.