Implement "Generalize empty list annotations" #1112

sjakobi · 2019-07-15T01:36:02Z

…as standardized in dhall-lang/dhall-lang#630

Fixes #414.
Fixes #770.

dhall/src/Dhall.hs

sjakobi · 2019-07-15T01:41:19Z

dhall/src/Dhall/Binary.hs

-        _T₁ = case _T₀ of
-            Nothing -> TNull
-            Just t  -> encode t
+        (label, _T₁) = case fmap Dhall.Core.denote _T₀ of


denote was required to get the parser tests to pass. I suspect the denoting should happen in the test setup though.

Usually we can assume that the expressions we encode here are already denoted, right?

We can enforce that in the types by changing the first type parameter of Expr to X

You mean changing the instance head to

instance ToTerm a => ToTerm (Expr X a)

?

I tried to do this and followed the type errors for a bit. Eventually there's some code in Dhall.Import that currently relies on an instance for Expr Src X. Maybe I'll revisit that idea later.

I realize now that the denoting here is only necessary because I stopped shallowDenoting the type in Dhall.Parser.Expression. I think the parser change was a good idea as we now have a more fully annotated parse tree.

Is it ok if I leave this code like it is now?

If we still want to change the ToTerm instance, we should do that separately, as that will be a good-sized change by itself.

I think you should either (A) denote the entire syntax tree once before decoding, rather than doing a denote here or (B) do a shallowDenote here. The main thing that I want to prevent is the inefficiency of multiple recursive denotes

Personally, I think (A) is simpler

(A) would mean that an already denoted Expr would get denoted again when we encode it. I'd rather change the instance head from Expr s a to Expr X a.

But that might cause some churn elsewhere – so I'm not too keen on it.

I think the denote here is ok: denote is very lazy, so it will only denote the List and the App, and be done.

If you disagree, I'd move shallowDenote into Dhall.Core and re-use it here.

In that case I think we should go with shallowDenote

Even though denote is lazy, if you have nested lists they will build up (i.e. the Nth nested list would have to step through N separate denote functions for each node in the abstract syntax tree). I know that this is unlikely to be an issue in practice, but it can't hurt to fix

sjakobi · 2019-07-15T01:45:12Z

dhall/src/Dhall/Core.hs

@@ -424,7 +424,7 @@ data Expr s a
    | TextShow
    -- | > List                                     ~  List
    | List
-    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t
+    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : t


These docs are a bit misleading: In the parser, we only insert the type into the ListLit when we have an empty list literal. I'm wondering why though!

Should there be an invariant that we have a Just t iff the list is empty?

Yes, there should be such an invariant

The more accurate way to encode things in the types would be to have separate Expr constructors for empty lists and non-empty lists, like:

| EmptyListLit (Expr s a) | NonEmptyListLit (NonEmptySeq (Expr s a))

... but that would be a more disruptive change

Actually, another way you could do this is to remove the type annotation entirely from the List constructor. In other words:

ListLit (Seq (Expr s a))

... and instead the type-checker can enforce that empty list literals are of the form Annot (ListList []) a

I think having a separate constructor for empty lists is much clearer. Should I open an issue to discuss the idea before I attempt implementing it?

@sjakobi: The main reason I suggest using Annot is because it's closer to the standard (since now an empty list without an annotation is a type error rather than a syntax error)

(since now an empty list without an annotation is a type error rather than a syntax error)

Do you suggest deviating from the standard here @Gabriel439?

Currently we still have tests/parser/failure/unit/ListLitEmptyAnnotation and the rule "[" whsp "]" whsp ":" whsp1 annotation-expression.

Oh, you're right, it is still part of the grammar. I still think splitting out the empty list constructor would be a bit disruptive, though.

dhall/src/Dhall/Diff.hs

dhall/src/Dhall/Parser/Expression.hs

dhall/src/Dhall/TypeCheck.hs

Gabriella439 · 2019-07-15T22:28:25Z

dhall/src/Dhall/Core.hs

@@ -424,7 +424,7 @@ data Expr s a
    | TextShow
    -- | > List                                     ~  List
    | List
-    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t
+    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : t


Yes, there should be such an invariant

The more accurate way to encode things in the types would be to have separate Expr constructors for empty lists and non-empty lists, like:

| EmptyListLit (Expr s a) | NonEmptyListLit (NonEmptySeq (Expr s a))

... but that would be a more disruptive change

Gabriella439 · 2019-07-15T22:45:13Z

dhall/src/Dhall/Core.hs

@@ -424,7 +424,7 @@ data Expr s a
    | TextShow
    -- | > List                                     ~  List
    | List
-    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t
+    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : t


Actually, another way you could do this is to remove the type annotation entirely from the List constructor. In other words:

ListLit (Seq (Expr s a))

... and instead the type-checker can enforce that empty list literals are of the form Annot (ListList []) a

dhall/src/Dhall/Diff.hs

dhall/src/Dhall/Pretty/Internal.hs

dhall/src/Dhall/TypeCheck.hs

dhall/tests/Dhall/Test/Parser.hs

sjakobi · 2019-07-16T12:21:23Z

The tests rely both on dhall-lang/dhall-lang#644 and dhall-lang/dhall-lang#641. I'll update the submodule once at least one of them has been merged.

sjakobi · 2019-07-20T11:50:51Z

Oops. I forgot to switch to shallowDenote! :/

…as standardized in dhall-lang/dhall-lang#630 Also: * Update the dhall-lang submodule to the state of dhall-lang/dhall-lang#654. * Skip the nonCharacter test for now. Fixes #414. Fixes #770.

sjakobi commented Jul 15, 2019

View reviewed changes

dhall/src/Dhall.hs Outdated Show resolved Hide resolved

sjakobi commented Jul 15, 2019

View reviewed changes

dhall/src/Dhall/Diff.hs Show resolved Hide resolved

sjakobi commented Jul 15, 2019

View reviewed changes

dhall/src/Dhall/Parser/Expression.hs Outdated Show resolved Hide resolved

sjakobi commented Jul 15, 2019

View reviewed changes

dhall/src/Dhall/TypeCheck.hs Outdated Show resolved Hide resolved

Gabriella439 reviewed Jul 15, 2019

View reviewed changes

sjakobi changed the title ~~WIP: Implement "Generalize empty list annotations"~~ Implement "Generalize empty list annotations" Jul 16, 2019

sjakobi self-assigned this Jul 20, 2019

sjakobi force-pushed the sjakobi/empty-list-annotations branch from 9d60c34 to ed6e334 Compare July 20, 2019 11:27

sjakobi added the merge me label Jul 20, 2019

sjakobi removed their assignment Jul 20, 2019

sjakobi force-pushed the sjakobi/empty-list-annotations branch from ed6e334 to b8ba141 Compare July 20, 2019 11:32

sjakobi mentioned this pull request Jul 20, 2019

Forbid invalid codepoints #1104

Merged

sjakobi removed the merge me label Jul 20, 2019

Implement "Generalize empty list annotations"

66ddc4a

…as standardized in dhall-lang/dhall-lang#630 Also: * Update the dhall-lang submodule to the state of dhall-lang/dhall-lang#654. * Skip the nonCharacter test for now. Fixes #414. Fixes #770.

sjakobi force-pushed the sjakobi/empty-list-annotations branch from b8ba141 to 66ddc4a Compare July 20, 2019 11:57

sjakobi added the merge me label Jul 20, 2019

sjakobi assigned sjakobi and unassigned sjakobi Jul 20, 2019

Gabriella439 approved these changes Jul 20, 2019

View reviewed changes

Merge branch 'master' into sjakobi/empty-list-annotations

0ea3e6f

mergify bot merged commit 0ee6ce6 into master Jul 20, 2019

mergify bot deleted the sjakobi/empty-list-annotations branch July 20, 2019 18:06

sjakobi mentioned this pull request Jul 20, 2019

Specialize Expr's ToTerm instance to (Expr X a) #1143

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement "Generalize empty list annotations" #1112

Implement "Generalize empty list annotations" #1112

sjakobi commented Jul 15, 2019 •

edited

Loading

sjakobi Jul 15, 2019

Gabriella439 Jul 15, 2019

sjakobi Jul 16, 2019

sjakobi Jul 16, 2019

sjakobi Jul 16, 2019

Gabriella439 Jul 19, 2019

sjakobi Jul 19, 2019

Gabriella439 Jul 19, 2019

sjakobi Jul 15, 2019

Gabriella439 Jul 15, 2019

Gabriella439 Jul 15, 2019

sjakobi Jul 16, 2019

Gabriella439 Jul 17, 2019

sjakobi Jul 18, 2019

Gabriella439 Jul 19, 2019

Gabriella439 Jul 15, 2019

Gabriella439 Jul 15, 2019

sjakobi commented Jul 16, 2019

sjakobi commented Jul 20, 2019

Implement "Generalize empty list annotations" #1112

Implement "Generalize empty list annotations" #1112

Conversation

sjakobi commented Jul 15, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sjakobi commented Jul 16, 2019

sjakobi commented Jul 20, 2019

sjakobi commented Jul 15, 2019 •

edited

Loading