[Agda] emptiness checking with strings

[Dan Licata]

Wow, that was fast!  Thanks! :)

Not to push my luck, but here's another feature request.  When using the
module system, the terms printed in error messages, goals, etc, get
pretty verbose.  Here's a sample from code I was just writing:

SatCtx
 (.lib.List.List.ListOpenInPrelude._::_
  (.lib.List.List.append
   (.lib.List.List.append .-1¦ô1
    (.lib.List.List.ListOpenInPrelude._::_
     (Types.HN
      (.lib.SumsProds.Prods.OpenInPrelude._,_
       .lib.List.List.ListOpenInPrelude.[]
       (Types._-1öò_ (Types.DA "nat")
        (Types._-1öò_ (Types.DA "nat") (Types.öñ (Types.DA "nat"))))))
     .lib.List.List.ListOpenInPrelude.[]))
   . (.lib.List.List.ListOpenInPrelude._::_
   (.lib.List.List.ListOpenInPrelude._::_
    (Types.HN
     (.lib.SumsProds.Prods.OpenInPrelude._,_
      .lib.List.List.ListOpenInPrelude.[]
      (Types._-1öò_ (Types.DA "ari") (Types.öñ (Types.DA "nat")))))
    .lib.List.List.ListOpenInPrelude.[])
   a)))

[My unicode got mangled in the cut and paste, but you get the idea.]

Ideally, I'd want Agda to try to print terms out using the names that
are in scope at the point of the goal/error, but I can imagine that it's
not keeping track of this information.

However, as a compromise, how about a toggle switch (like
agda2-display-implicit-arguments) that suppresses the full path, just
printing the original name at the end of it?  This wouldn't have as much
information as above (e.g., it would be impossible to distinguish
multiple _::_ from different modules), but it would be nice for
situations like this, if the user keeps this caveat in mind.

The above would look like:

SatCtx
 (_::_
  (append
   (append .-1¦ô1
    (_::_
     (Types.HN
      (._,_
       []
       (Types._-1öò_ (Types.DA "nat")
        (Types._-1öò_ (Types.DA "nat") (Types.öñ (Types.DA "nat"))))))
     []))
   . (_::_
   (_::_
    (Types.HN
     (_,_
      []
      (Types._-1öò_ (Types.DA "ari") (Types.öñ (Types.DA "nat")))))
    [])
   a)))

What do you think?
-Dan

On Jan31, Ulf Norell wrote:
> On Jan 31, 2008 2:09 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> 
> > Hi everyone,
> >
> > Given the usual equality type Id M N and the empty type Void, I'd like
> > to write a function
> >
> > contra : Id "nat" "exp" -> Void
> > contra ()
> >
> > However, the emptiness checker doesn't notice that this type is
> > uninhabited (like it would if "nat" and "exp" were two different
> > constructors of a datatype).
> >
> > Does anyone know a workaround?  Also, would it be hard to catch this
> > case (i.e., treat string literals as constructors), or is this just a
> > feature that's not implemented yet?
> 
> 
> It wouldn't be hard at all. In fact a patch has just been pushed that fixes
> the issue.
> 
> / Ulf

> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


>  LocalWords:  ListOpenInPrelude