Dhall-haskell: dhall-docs jump to definition of names introduced by `Lam` and `Pi` constructor

[german1608]

I'd like to work on this, but currently the Lam and Pi constructor don't have the Src or SourcePos of the parsed label.

There are two ways to solve this:

• Record the whitespace on Lam and Pi bindings similar to what we do on Binding. This will help in the context of #145
  The new constructors would look roughly like this:
  haskell data FunctionBinding = FunctionBinding {...} data Expr s a = ... | Lam (Maybe s, Text) (Expr s a) (Expr s a) | Pi (Maybe s, Text) (Expr s a) (Expr s a) ....
• Use the parent Note Src of the Lam or Pi expression and run a parser to get the relative location of the label in the src and add it to the srcStart. This would only affect dhall-docs and it's somewhat similar to how dhall-lsp-server computes the source spans for source code messages.

What do you think is the best way to tackle this? cc: @sjakobi @Gabriel439 @Profpatsch

[sjakobi]

• Record the whitespace on Lam and Pi bindings similar to what we do on Binding. This will help in the context of #145
  The new constructors would look roughly like this:
  haskell data FunctionBinding = FunctionBinding {...} data Expr s a = ... | Lam (Maybe s, Text) (Expr s a) (Expr s a) | Pi (Maybe s, Text) (Expr s a) (Expr s a) ....

Could you flesh out that code a bit? Where is FunctionBinding used in Expr? Could you produce examples similar to what we have in the haddocks for Binding?

• Use the parent Note Src of the Lam or Pi expression and run a parser to get the relative location of the label in the src and add it to the srcStart. This would only affect dhall-docs and it's somewhat similar to how dhall-lsp-server computes the source spans for source code messages.

This sounds as if it could be implemented much faster.

I guess Gabriel's golden rule of software quality suggests the first option though. And we could indeed use your work to make progress on #145.

While the RecordField refactoring probably wasn't a lot of fun, I suspect doing something similar for Lam and Pi would be much easier for you now.

[Gabriel439]

One possible thing to consider is that the current way of encoding these annotation is a bit weakly-typed. Specifically, while we can guarantee that the Just constructor for a value of type Maybe s is uninhabited when s = Void, we cannot guarantee that the Just is inhabited when s = Src. Similarly, we cannot guarantee that if one source span is present then the other ones are also present.

One extreme way to solve that problem would be to keep two separate expression types, one without any Note constructors or Src spans and one with all of the Src spans. I don't know if there is a simpler solution, though.

[german1608]

Could you flesh out that code a bit? Where is FunctionBinding used in Expr? Could you produce examples similar to what we have in the haddocks for Binding?

Oops:

-- | > ∀( {- A -} a {- B -} : T) -> e ~ FunctionBinding "{- A -}" "a" "{- B -}"
data FunctionBinding s = FunctionBinding
    { functionBindingSrc0 :: Maybe s
    , label :: Text
    , functionBindingSrc :: Maybe s
    }
data Expr s a
    = ...
    | Lam (FunctionBinding s) (Expr s a) (Expr s a)
    | Pi (FunctionBinding s) (Expr s a) (Expr s a)
    ....

[german1608]

Similarly, we cannot guarantee that if one source span is present then the other ones are also present.

This could be solved by wrapping all source spans in the same Maybe constructor to ensure atomicity: either all are present or none. Sadly that doesn't solve all our problems

[Gabriel439]

@german1608: That would work for one constructor, but we'd also like to guarantee that all constructors within the syntax tree also stay in sync with respect to whether or not they have Src spans.

[german1608]

@Gabriel439: Although what you're suggesting to solve is important, we could tackle that in another moment. Maybe record an issue to not forget that?

[Gabriel439]

@german1608: Yeah, it's not urgent. If we work within the existing set of solutions then I would recommend adding additional Maybe fields to Lam/Pi

[Gabriel439]

Also, to make things more ergonomic, it might help to use PatternSynonyms to make the transition smoother for end users. For example, we could create new Lam/Pi pattern synonyms representing the old behavior and then make LamAnnot/PiAnnot the underlying constructors with the full annotations. Then you wouldn't need smart constructors/destructors.

[german1608]

Cool. I'll read about that. Thanks @Gabriel439

[Gabriel439]

You're welcome! 🙂

[german1608]

I have a doubt about pattern synonyms, and although I don't like posting coding questions here on GitHub issues I'll do so since I don't have enough for a Draft PR :smile:

---

I changed the Lam type constructor to the following:

data FunctionBinding s a = FunctionBinding
    { fbSrc0 :: Maybe s
    , fbVariable :: Text
    , fbSrc1 :: Maybe s
    , fbSrc2 :: Maybe s
    , fbAnnotation :: Expr s a
    } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable)

data Expr s a = ... | LamAnnot (FunctionBinding s a) (Expr s a) | ...

...and I added the following pattern for backwards compatibility:

pattern Lam :: Text -> Expr s a -> Expr s a -> Expr s a
pattern Lam l t e <- LamAnnot (FunctionBinding _ l _ _ t) e
  where
    Lam l t e = LamAnnot (FunctionBinding Nothing l Nothing Nothing t) e

and in an usage of the Lam constructor on other module of the dhall package, I got this warning:

/home/german/Documents/gsoc/dhall-haskell/dhall/src/Dhall/Binary.hs:596:12: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (LamAnnot _ _)
    |       
596 |     go e = case e ofa
    |            ^^^^^^^^^...

I enabled PatternSynonyms and imported the Lam pattern on that module before compiling to get that error. In that case clause there is a branch for Lam l t s. Why does GHC reports that? Isn't the Lam pattern enough to cover all cases?

[Gabriel439]

@german1608: You will also want a COMPLETE pragma:

https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-pragmas

[german1608]

@Gabriel439: Forgot to post here, I tried using that pragma specifying _all_ constructors but I got this warning from GHC:

Pattern match checker exceeded (2000000) iterations

the full GHC log is lost sadly, I moved on and decided to tackle the pattern synonym issue later. Do you know what could be the reason for that?

[Gabriel439]

@german1608: No idea :\

Yeah, then go ahead with your original plan, then

[sjakobi]

Pattern match checker exceeded (2000000) iterations

This looks similar to the issue I recorded here:

https://github.com/dhall-lang/dhall-haskell/blob/42b119d245d6fb3c71d1fb184df346f8e3a6df52/dhall/src/Dhall/Syntax.hs#L589-L606

This was fixed in GHC 8.10.

[german1608]

(moving the discuss from #1980 here as @sjakobi suggested)

(And I somewhat feel that an issue #1978 would be the better, more permanent place for such discussions.)

I think it would also be useful for this discussion to have a motivating example that benefits from having comments on a Pi.

The motivation of #1980 is more in favor of dhall-docs rather than on #145. I use these Src span to compute the label position. In order to get jump-to-definition right, I need to be able to get the SourcePoses of the target elements

I don't feel like anybody would write comments for Lam in the place where this PR aims to preserve, and the same applies for Pi (on the ∀(x : A) -> B case), but it doesn't do any damage to do so anyway. A more direct solution specific for dhall-docs is to just record the start and end position of the label with no whitespace, but since we already have Binding and RecordField I feel that introducing SourcePos on the Lam (and Pi) constructor doesn't follow that pattern and it doesn't help in #145.