Discussion:
INLINE-pragma
(too old to reply)
Frederik Hanghøj Iversen
2018-02-21 14:40:16 UTC
Permalink
Raw Message
I know there's an INLINE-pragma for Agda (though it's not documented here
[1]). This pragma affects compilation. I wonder if there was something akin
to this for type-checking.

When I want to close a goal with a complex type I usually spend a
considerable time defining helper functions and in particular figuring out
what type these should have. Agda of course can help me here, but often it
doesn't display the type that I want. The best type is rarely the
non-normalized *nor* fully normalized type. Ideally I would like to be able
to step up and down these types interactively. But something perhaps easier
to implement and also super helpful would be if I could e.g. mark a "type
synonym" as being completely transparent, so that it's definition would be
inlined when I ask for goal and context.

As a super small example of what I'm looking for is:

Assume I have a type-synonym `P T = A × T' and I want to close a hole of
type `P T` then `C-c C-,` should give me `Goal: A × T`. Incidentally if I
issue `C-u C-u C-c C-,` the hole will be displayed as `Σ A (λ x → T)` which
is less helpful. Granted in this case the type is easily understood - but
this is rarely the case.

[1]: http://agda.readthedocs.io/en/latest/language/pragmas.html
--
Regards
*Frederik HanghÞj Iversen*
Frederik Hanghøj Iversen
2018-03-02 15:26:54 UTC
Permalink
Raw Message
In-line with the above idea I wonder if there is an option to do something
in the middle between fully normalizing a goal and not normalizing it.

Is it possible to normalize something to the first visible constructors?
Say I have declared a function that is not visible in my current scope. The
function is defined in terms of other functions that are visible in scope.
Can I get Agda to show me the visible type?

MWE:

module _ where

open import Data.Product

module _ {C O M P L E X : Set} where
private
T = C × O × M × P × L × E × X
ex : T → X
ex (c , o , m , p , l , e , x) = x

x : {X : Set} → X
x = ex {!!}

In this goal I want to be the type displayed to me to be as if `T` had been
inlined in the definition of `ex`. In this case it's a septuple with
elements corresponding to the implicit parameters at the usage-site of
`ex`. This is just a contrived example but it highlights what I'm after.

On Wed, Feb 21, 2018 at 3:40 PM, Frederik HanghÞj Iversen <
Post by Frederik Hanghøj Iversen
I know there's an INLINE-pragma for Agda (though it's not documented here
[1]). This pragma affects compilation. I wonder if there was something akin
to this for type-checking.
When I want to close a goal with a complex type I usually spend a
considerable time defining helper functions and in particular figuring out
what type these should have. Agda of course can help me here, but often it
doesn't display the type that I want. The best type is rarely the
non-normalized *nor* fully normalized type. Ideally I would like to be able
to step up and down these types interactively. But something perhaps easier
to implement and also super helpful would be if I could e.g. mark a "type
synonym" as being completely transparent, so that it's definition would be
inlined when I ask for goal and context.
Assume I have a type-synonym `P T = A × T' and I want to close a hole of
type `P T` then `C-c C-,` should give me `Goal: A × T`. Incidentally if I
issue `C-u C-u C-c C-,` the hole will be displayed as `Σ A (λ x → T)` which
is less helpful. Granted in this case the type is easily understood - but
this is rarely the case.
[1]: http://agda.readthedocs.io/en/latest/language/pragmas.html
--
Regards
*Frederik HanghÞj Iversen*
--
Regards
*Frederik HanghÞj Iversen*
Nils Anders Danielsson
2018-03-06 10:14:05 UTC
Permalink
Raw Message
Post by Frederik Hanghøj Iversen
Is it possible to normalize something to the first visible
constructors?
I don't think there's any support for that at the moment. Perhaps you
could try to implement it yourself.
--
/NAD
Loading...