[Agda] The joys and sorrows of abstraction

[Arseniy Alekseyev]

(and to be sure, [abstract] keyword is not the issue here: this manifests
no matter how you achieve abstraction: module parameter, lambda, whatever)

On 17 May 2018 at 00:01, Arseniy Alekseyev <arseniy.alekseyev at gmail.com>
wrote:

> I'll point out that source-level stability under substitution is not even
> compatible with implicit parameters if unsolved metavariables is also
> something you care about.
> For example the below program works with "abstract" and has unsolved
> metavariables without "abstract".
>
> data Bool : Set where
>   true false : Bool
>
> abstract
>   or : Bool → Bool → Bool
>   or true _ = true
>   or false x = x
>
> data Is-bool : Bool → Set where
>   is-bool : ∀ x → Is-bool x
>
> contrived : ∀ {x} → Is-bool (or x true) → Bool
> contrived {x} _ = x
>
> z = contrived (is-bool (or false true))
>
>
> On 16 May 2018 at 22:58, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
>>
>>
>> On 16/05/18 22:55, apostolis.xekoukoulotakis at gmail.com wrote:
>>
>>> This is really scary, for good reason. It seems that we are in a better
>>> position now than a few years ago.
>>>
>>> I do remember as an undergraduate, thinking that all I need is to start
>>> from the fundamentals of Mathematics and then prove all of the rest.
>>> Then , I found that the fundamentals were full of paradoxes.
>>> https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou
>>> ndational_crisis
>>>
>>
>> Agda is an incarnation of both established type theories and frontier
>> research on possible new type theories, and it is good that things are like
>> this, because researchers can use it for experimentation.
>>
>> But some other researchers would like to use Agda to work with
>> established type theories.
>>
>> It is good that Agda has some seat-belts such as --exact-split, --safe,
>> and --without-K, for that purpose.
>>
>> Further seat-belts would be welcome.
>>
>> The point I was making was not about scariness but about awareness. If
>> you use a feature beyond your type-theory expertise, consider whether this
>> feature is well established, but unknown to you, or something experimental
>> and perhaps not well-defined.
>>
>> Martin
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180517/20484264/attachment.html>