[Agda] question about instance arguments

Peter Selinger selinger at mathstat.dal.ca
Thu Dec 4 17:45:44 CET 2014


I've updated this page of the reference manual accordingly:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments

-- Peter

Andreas Abel wrote:
> 
> On 04.12.2014 14:42, Peter Selinger wrote:
> > Oops, I just read further in the Changelog, and I believe I found the
> > answer to my question:
> >
> >   * Constructors of records and datatypes are automatically added to
> >     the instance table.
> 
> This is a temporary glitch, valid for Agda 2.4.2 - 2.4.2.2, but will 
> change in the next major release
> 
>    https://code.google.com/p/agda/issues/detail?id=1267
> 
> In Agda 2.4.3 (master on github), you have to write
> 
>   data _<:_ : Set -> Set -> Set₁ where
>     instance
>       <:-base : {A : Set} -> A <: A
>       <:-step : {A B : Set} -> {{p : A <: B}} -> A <: Succ B
> 
> > Also:
> >
> >    Instance search takes into account all local bindings and all global
> >    'instance' bindings and the search is recursive.
> >
> > This explains why "let e = eqBool in true == true" worked in my
> > previous example. I may have a shot of making some updates to the
> > reference manual. -- Peter
> 
> Thanks!
> I might want to mention the upcoming change in treatment of constructors.
> 
> Cheers,
> Andreas
> 
> > Peter Selinger wrote:
> >>
> >> Hi Dominique and Andreas,
> >>
> >> thanks for the replies. The actual behavior from Agda I experience is
> >> a bit erratic. Sometimes it will recognize identifiers in scope even
> >> without the "instance" keyword, and sometimes it won't.
> >>
> >> What is the syntax for using an "instance" keyword with data type
> >> definitions? Do you make the whole data type an instance, or just
> >> individual constructors? Consider the following example:
> >>
> >> module InstanceTest where
> >>
> >>    -- Zero is the empty set.
> >>    data Zero : Set where
> >>
> >>    -- Succ A = A + 1. In other words, Succ, zero, and succ are what is
> >>    -- usually called Maybe, nothing, and just.
> >>    data Succ A : Set where
> >>      zero : Succ A
> >>      succ : A -> Succ A
> >>
> >>    -- A subtyping relation: less-than-or-equal with respect to Succ.
> >>    data _<:_ : Set -> Set -> Set₁ where
> >>      <:-base : {A : Set} -> A <: A
> >>      <:-step : {A B : Set} -> {{p : A <: B}} -> A <: Succ B
> >>
> >>    -- Cast from a smaller to a larger type.
> >>    cast : {A B : Set} -> {{p : A <: B}} -> A -> B
> >>    cast {{<:-base}} a = a
> >>    cast {{<:-step}} a = succ (cast a)
> >>
> >>    test : {A : Set} -> A -> Succ (Succ (Succ A))
> >>    test x = cast x
> >>
> >> The point about the subtyping relation <: is that if it exists, it is
> >> uniquely inhabited; however, with ordinary implicit arguments, Agda's
> >> type checker would not be able to infer this. With instance arguments,
> >> this works handsomely. Note how the subtyping was automatically
> >> inferred in the definition of "test".
> >>
> >> However, I have not used any "instance" keywords here. Does this
> >> contradict the stated behavior of Agda 2.4.2? Also, putting an
> >> "instance" keyword before either "data" or "<:-base" or "<:-step"
> >> gives a parsing error in all cases. So is the above syntax still
> >> considered correct for Agda 2.4.2? If not, what is the alternative?
> >>
> >> Thanks, -- Peter
> >>
> >> Dominique Devriese wrote:
> >>>
> >>> Peter,
> >>>
> >>> Firstly, the problem you're having is a result of the changes to
> >>> instance argument semantics that have been made in Agda 2.4.2, which
> >>> are not yet reflected in the reference manual and some of the error
> >>> messages.  You can look at
> >>>
> >>> https://github.com/agda/agda/blob/2.4.2.2/CHANGELOG
> >>>
> >>> (look for "Instance search") to see what has been changed.
> >>>
> >>> 2014-12-04 2:28 GMT+01:00 Peter Selinger <selinger at mathstat.dal.ca>:
> >>>> I'm trying to learn to use instance arguments, and I tried a first
> >>>> example, essentially taken from the reference manual:
> >>>>
> >>>> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Modell> ingTypeClassesWithInstanceArguments
> >>>>
> >>>> Unfortunately, I cannot get it to work. Probably I am overlooking
> >>>> something terribly simple. I am using Agda version 2.4.2.2, freshly
> >>>> installed via Cabal.
> >>>
> >>> Yes, the reference manual needs updating.
> >>>
> >>>> Here's my file:
> >>>>
> >>>> module EqTest where
> >>>>
> >>>>    data Bool : Set where
> >>>>      true : Bool
> >>>>      false : Bool
> >>>>
> >>>>    eq : Bool -> Bool -> Bool
> >>>>    eq true true = true
> >>>>    eq false false = true
> >>>>    eq _ _ = false
> >>>>
> >>>>    record Eq (t : Set) : Set where
> >>>>      field
> >>>>        _==_ : t -> t -> Bool
> >>>>
> >>>>    open Eq {{...}}
> >>>>
> >>>>    eqBool : Eq Bool
> >>>>    eqBool = record { _==_ = eq }
> >>>
> >>> Essentially, you need to change this to
> >>>     instance eqBool : Eq Bool
> >>>     eqBool = record { _==_ = eq }
> >>>
> >>>>    test1 = true == true
> >>>
> >>>> The error message I receive, in the test1 line, is:
> >>>>
> >>>> /home/selinger/projects/lang/agda/EqTest.agda:21,16-18
> >>>> No variable of type Eq Bool was found in scope.
> >>>> when checking that true true are valid arguments to a function of
> >>>> type {t : Set} {{r : Eq t}} → t → t → Bool
> >>>>
> >>>> This seems contradictory, since the variable eqBool is indeed in
> >>>> scope.
> >>>
> >>> It would probably be a good idea to change this error message to
> >>> something like "... was found using the instances in scope"?
> >>>
> >>>> If I replace the eqBool definition by a postulate, as in the
> >>>> reference manual,
> >>>>
> >>>>    postulate eqBool : Eq Bool
> >>>>
> >>>> I get the same error message.
> >>>
> >>> Yes, this makes no difference.
> >>>
> >>>> On the other hand, if I write
> >>>>
> >>>>    test1 = let e = eqBool in true == true
> >>>>
> >>>> the error disappears in both cases.
> >>>
> >>> Ah, this surprises me, I thought you had to annotate let-bound
> >>> variables as well using instance under the new schem.
> >>>
> >>>> On the other hand, this does not
> >>>> work:
> >>>>
> >>>>    test1 = true == true
> >>>>      where e = eqBool
> >>>
> >>> This is expected under the new semantics.
> >>>
> >>>> The reference manual says:
> >>>>
> >>>> "A candidate expression is any identifier (possibly applied to a
> >>>> hidden argument) in scope (either imported or defined previously in
> >>>> the file) or in the context (e.g. section arguments or arguments of
> >>>> the current function)."
> >>>>
> >>>> My example seems to contradict that. Is it a bug?
> >>>
> >>> Yes, it is a bug in the reference manual :).  It should be updated to
> >>> reflect the new semantics.
> >>>
> >>> Dominique
> >>>
> >>
> >>
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> 



More information about the Agda mailing list