[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