ucm command: view only type signature

[ceedubs]

I find that I'm often just interested in the type signature of a term, but when I view myTerm the implementation is long enough that I have to page back to see the type signature. It'd be nice to have an easy way to view just the type signature.

For example instead of:

.> view .base.List.map

  base.List.map : (a ->{𝕖} b) -> [a] ->{𝕖} [b]
  base.List.map f a =
    go i as acc =
      match List.at i as with
        None   -> acc
        Some a ->
          use Nat +
          go (i + 1) as (acc :+ f a)
    go 0 a []

I'd want something like:

.> signature .base.List.map

  base.List.map : (a ->{𝕖} b) -> [a] ->{𝕖} [b]

Some possible command names that come to mind:

• signature List.map
• view.signature List.map
• view : List.map (similar to using find : to find by type, but I think that this is unnecessarily cryptic and don't really like it)
• type List.map
• typeOf List.map
• view.type List.map

NOTE: if the fzf completion options showed the type signature when doing the no-arg version of view that would probably be good enough for me and I don't know that I'd feel the need for a separate command.

[emilhotkowski]

1. Do you want to add this to UCM?
2. Which option do we prefer? (adding new command is easy IMO by adding parameter to HandleShowDefinition function onlyType or something similar )

If this is for grab then I can do it.

[ceedubs]

@emilhotkowski Thanks that would be great! My inclination would be to add a view.signature command to ucm. But I can't speak for others.

[emilhotkowski]

I'll add code that can handle this option, but if we choose differently it should be easy to fix PR.

[hojberg]

a view.summary version might be a separate option here that allows you to view summaries of types as well as terms.

so like unique type Nonempty a might be the summary of unique type Nonempty a = Nonempty a [a] or something like that.

We use something similar to this in the UI for showing results in the Finder (and eventually for hovers).

[emilhotkowski]

If we need something more complicated then what I thought than I'd need some guidance to implement this 🤪