[Agda] question about instance arguments
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Dec 4 21:30:23 CET 2014
Excellent! Big thanks. --Andreas
On 04.12.2014 17:45, Peter Selinger wrote:
> 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/
>>
>
--
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