[Agda] question about instance arguments
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Dec 4 15:29:49 CET 2014
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