[Agda] Small Kernel

[a.j.rouvoet]

Hi Xuanrui,

But it would probably be fair to say (I think?) that if we were to 
count, it would be extremely surprising if Agda's core turns out to be 
lighter than Coq's. Much of the apparent weight of Coq is in the tactic 
language, various typeclass mechanisms etc, which are distinctly not 
part of the kernel.

Best,

Arjen

On 12/4/19 10:35 AM, Jesper Cockx wrote:
> Hi Xuanrui,
>
> It's very hard to measure because as I said, most parts of Agda's core 
> don't have an independent typechecker, so all the code is mixed up 
> with the elaboration of user code to internal syntax.
>
> -- Jesper
>
> On Wed, Dec 4, 2019 at 10:18 AM Xuanrui Qi <xuanrui at nagoya-u.jp 
> <mailto:xuanrui at nagoya-u.jp>> wrote:
>
>     Hi Jesper, Hi Yotam,
>
>     I wonder, how large, in total, are those components that could be
>     considered part of the "kernel" of Agda? I know that Coq's kernel is
>     quite large (>10000 lines OCaml), but Agda seems a much lighter system
>     than Coq so I expect the number to be much smaller?
>
>     Best,
>     Xuanrui
>
>     On Wed, 2019-12-04 at 10:13 +0100, Jesper Cockx wrote:
>     > Hi Yotam,
>     >
>     > It is true that Agda currently has a much shakier foundation
>     than say
>     > Coq or Lean. It does have an internal term syntax that could be seen
>     > as a core language (
>     >
>     https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs
>     > ). It even has an independent typechecker for internal syntax (
>     >
>     https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs
>     > ).
>     >
>     > However, this story is far from complete because it takes the
>     > signature of defined types and functions for granted. In particular,
>     > functions by dependent pattern matching are represented as case
>     trees
>     > that need to pass coverage checking and termination checking, which
>     > means those checks are also part of Agda's 'trusted core'. In our
>     > ICFP paper last year (
>     > https://dl.acm.org/citation.cfm?doid=3243631.3236770) Andreas and I
>     > describe a potential core language for case trees, but so far there
>     > is no independent typechecker for case trees as we have for internal
>     > syntax (one day...).
>     >
>     > Another important part of Agda's trusted core is the conversion
>     > checker, which in Agda shares most code with the constraint solver (
>     >
>     https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs
>     > ), while in Coq it's two separate algorithms. Recently I added the
>     > possibility to run the conversion checker in 'pure' mode which is
>     > guarateed to be free of side-effects (
>     >
>     https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs
>     > ).
>     >
>     > As you can see, there is bits and pieces that could be part of a
>     core
>     > language of Agda, but no real coherent story yet. In general, any
>     > attempt to build a core language will also be an exercise in
>     > selecting which features of Agda should be included and which ones
>     > should not (e.g. irrelevance, sized types, prop, rewrite rules,
>     > cubical, ...). Yet this selection of various features would've been
>     > much harder to implement if Agda already had a core language
>     from the
>     > beginning, so not having a core language has advantages as well as
>     > disadvantages.
>     >
>     > All the best,
>     > Jesper
>     >
>     > On Tue, Dec 3, 2019 at 6:05 PM Yotam Dvir
>     <yotamdvir at mail.tau.ac.il <mailto:yotamdvir at mail.tau.ac.il>>
>     > wrote:
>     > > Hi there,
>     > >
>     > > I am interested in the soundness of Agda as a proof-assistant. To
>     > > my understanding Agda development veers more in the direction of
>     > > interesting abstractions and advanced programming features, at the
>     > > cost of less solid foundations.
>     > >
>     > > Is this understanding correct?
>     > > How close is Agda to having a so-called "small kernel”, and how
>     > > does it compare to other proof-assistants such as Coq and HOL
>     > > Light?
>     > >
>     > > (You are also welcome to answer on cstheory.stackexchange.)
>     > >
>     > > Thanks in advance!
>     > > _______________________________________________
>     > > Agda mailing list
>     > > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     > > https://lists.chalmers.se/mailman/listinfo/agda
>     >
>     > _______________________________________________
>     > Agda mailing list
>     > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     > https://lists.chalmers.se/mailman/listinfo/agda
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191204/5783d7b0/attachment.html>