[Agda] The joys and sorrows of abstraction

[Arseniy Alekseyev]

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/13083b19/attachment.html>