[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