Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement "Generalize empty list annotations" #1112

Merged
merged 2 commits into from
Jul 20, 2019
Merged

Implement "Generalize empty list annotations" #1112

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
66ddc4a
Implement "Generalize empty list annotations"
sjakobi Jul 15, 2019
0ea3e6f
Merge branch 'master' into sjakobi/empty-list-annotations
mergify[bot] Jul 20, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion dhall/dhall-lang
Open in desktop
Submodule dhall-lang updated 34 files
+0 −14 Prelude/Map.dhall
+66 −0 Prelude/XML/Type
+3 −0 Prelude/XML/attribute
+67 −0 Prelude/XML/element
+3 −0 Prelude/XML/emptyAttributes
+32 −0 Prelude/XML/leaf
+19 −0 Prelude/XML/package.dhall
+69 −0 Prelude/XML/render
+41 −0 Prelude/XML/text
+3 −0 Prelude/package.dhall
+1 −1 standard/README.md
+2 −2 standard/alpha-normalization.md
+34 −20 standard/beta-normalization.md
+14 −1 standard/binary.md
+61 −8 standard/dhall.abnf
+2 −2 standard/shift.md
+2 −2 standard/substitution.md
+3 −3 standard/type-inference.md
+1 −1 tests/normalization/success/unit/ListNormalizeTypeAnnotationA.dhall
+1 −1 tests/normalization/success/unit/ListNormalizeTypeAnnotationB.dhall
+1 −0 tests/normalization/success/unit/RecordProjectionNormalizeFieldsA.dhall
+1 −0 tests/normalization/success/unit/RecordProjectionNormalizeFieldsB.dhall
+1 −0 tests/parser/failure/nonCharacter.dhall
+4 −0 tests/parser/failure/nonUtf8.dhall
+0 −0 tests/parser/success/unit/ListLitEmpty1A.dhall
+ − tests/parser/success/unit/ListLitEmpty1B.dhallb
+1 −0 tests/parser/success/unit/ListLitEmpty2A.dhall
+ − tests/parser/success/unit/ListLitEmpty2B.dhallb
+0 −0 tests/parser/success/unit/ListLitEmptyPrecedenceA.dhall
+ − tests/parser/success/unit/ListLitEmptyPrecedenceB.dhallb
+1 −0 tests/type-inference/success/unit/ListLiteralEmptyNormalizeAnnotationA.dhall
+1 −0 tests/type-inference/success/unit/ListLiteralEmptyNormalizeAnnotationB.dhall
+1 −0 tests/typecheck/failure/unit/OptionalDeprecatedSyntaxAbsent.dhall
+1 −0 tests/typecheck/failure/unit/OptionalDeprecatedSyntaxPresent.dhall
15 changes: 10 additions & 5 deletions dhall/src/Dhall/Binary.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ import qualified Control.Monad as Monad
import qualified Data.ByteArray
import qualified Data.ByteString
import qualified Data.Sequence
import qualified Dhall.Core
import qualified Dhall.Map
import qualified Dhall.Set
import qualified Options.Applicative
Expand Down Expand Up @@ -281,12 +282,13 @@ instance ToTerm a => ToTerm (Expr s a) where
l₁ = encode l₀
r₁ = encode r₀
encode (ListLit _T₀ xs₀)
| null xs₀ = TList [ TInt 4, _T₁ ]
| null xs₀ = TList [ TInt label, _T₁ ]
| otherwise = TList ([ TInt 4, TNull ] ++ xs₁)
where
_T₁ = case _T₀ of
Nothing -> TNull
Just t -> encode t
(label, _T₁) = case fmap Dhall.Core.shallowDenote _T₀ of
Nothing -> (4 , TNull)
Just (App t0 t1) | List <- Dhall.Core.shallowDenote t0 -> (4 , encode t1)
Just t -> (28, encode t)

xs₁ = map encode (Data.Foldable.toList xs₀)
encode (Some t₀) =
Expand Down Expand Up @@ -614,7 +616,7 @@ instance FromTerm a => FromTerm (Expr s a) where
return (op l₀ r₀)
decode (TList [ TInt 4, _T₁ ]) = do
_T₀ <- decode _T₁
return (ListLit (Just _T₀) empty)
return (ListLit (Just (App List _T₀)) empty)
decode (TList (TInt 4 : TNull : xs₁ )) = do
xs₀ <- traverse decode xs₁
return (ListLit Nothing (Data.Sequence.fromList xs₀))
Expand Down Expand Up @@ -780,6 +782,9 @@ instance FromTerm a => FromTerm (Expr s a) where
t₀ <- decode t₁
_T₀ <- decode _T₁
return (ToMap t₀ (Just _T₀))
decode (TList [ TInt 28, _T₁ ]) = do
_T₀ <- decode _T₁
return (ListLit (Just _T₀) empty)
decode _ =
empty

Expand Down
19 changes: 12 additions & 7 deletions dhall/src/Dhall/Core.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ module Dhall.Core (
, isNormalized
, isNormalizedWith
, denote
, shallowDenote
, freeIn

-- * Pretty-printing
Expand Down Expand Up @@ -426,7 +427,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
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

-- > ListLit Nothing [x, y, z] ~ [x, y, z]
| ListLit (Maybe (Expr s a)) (Seq (Expr s a))
-- | > ListAppend x y ~ x # y
Expand Down Expand Up @@ -1292,6 +1293,10 @@ denote (Project a b ) = Project (denote a) (fmap denote b)
denote (ImportAlt a b ) = ImportAlt (denote a) (denote b)
denote (Embed a ) = Embed a

shallowDenote :: Expr s a -> Expr s a
shallowDenote (Note _ e) = shallowDenote e
shallowDenote e = e

{-| Reduce an expression to its normal form, performing beta reduction and applying
any custom definitions.

Expand Down Expand Up @@ -1417,7 +1422,7 @@ normalizeWithM ctx e0 = loop (denote e0)
(ListAppend (ListLit Nothing (pure "a")) "as")
)

nil = ListLit (Just _A₀) empty
nil = ListLit (Just (App List _A₀)) empty
App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do
t' <- loop t
if boundedType t' then strict else lazy
Expand All @@ -1443,7 +1448,7 @@ normalizeWithM ctx e0 = loop (denote e0)
o = case Data.Sequence.viewr ys of
_ :> y -> Some y
_ -> App None t
App (App ListIndexed _A₀) (ListLit _A₁ as₀) -> loop (ListLit t as₁)
App (App ListIndexed _A₀) (ListLit _ as₀) -> loop (ListLit t as₁)
where
as₁ = Data.Sequence.mapWithIndex adapt as₀

Expand All @@ -1453,7 +1458,7 @@ normalizeWithM ctx e0 = loop (denote e0)
, ("value", _A₀)
]

t | null as₀ = Just _A₂
t | null as₀ = Just (App List _A₂)
| otherwise = Nothing

adapt n a_ =
Expand All @@ -1465,7 +1470,7 @@ normalizeWithM ctx e0 = loop (denote e0)
App (App ListReverse t) (ListLit _ xs) ->
loop (ListLit m (Data.Sequence.reverse xs))
where
m = if Data.Sequence.null xs then Just t else Nothing
m = if Data.Sequence.null xs then Just (App List t) else Nothing
App (App (App (App (App OptionalFold _) (App None _)) _) _) nothing ->
loop nothing
App (App (App (App (App OptionalFold _) (Some x)) _) just) _ ->
Expand Down Expand Up @@ -1697,8 +1702,8 @@ normalizeWithM ctx e0 = loop (denote e0)
let keyValues = Data.Sequence.fromList (map entry (Dhall.Map.toList kvsX))

let listType = case t' of
Just (App List itemType) | null keyValues ->
Just itemType
Just _ | null keyValues ->
t'
_ ->
Nothing

Expand Down
7 changes: 2 additions & 5 deletions dhall/src/Dhall/Diff.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ module Dhall.Diff (
) where

import Data.Foldable (fold, toList)
import Data.Function (on)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Monoid (Any(..))
import Data.Semigroup
Expand Down Expand Up @@ -573,8 +572,6 @@ skeleton (ListLit {}) =
<> " "
<> colon
<> " "
<> builtin "List"
sjakobi marked this conversation as resolved.
Show resolved Hide resolved
<> " "
<> ignore
skeleton (ListAppend {}) =
ignore
Expand Down Expand Up @@ -778,11 +775,11 @@ diffAnnotatedExpression l r@(ToMap {}) =
diffAnnotatedExpression (ListLit aL@(Just _) bL) (ListLit aR bR) = align doc
where
doc = format " " (diffList bL bR)
<> format " " (diffMaybe (colon <> " ") (diffApplicationExpression `on` App List) aL aR)
<> format " " (diffMaybe (colon <> " ") diffApplicationExpression aL aR)
diffAnnotatedExpression (ListLit aL bL) (ListLit aR@(Just _) bR) = align doc
where
doc = format " " (diffList bL bR)
<> format " " (diffMaybe (colon <> " ") (diffApplicationExpression `on` App List) aL aR)
<> format " " (diffMaybe (colon <> " ") diffApplicationExpression aL aR)
diffAnnotatedExpression l@(Annot {}) r@(Annot {}) =
enclosed' " " (colon <> " ") (docs l r)
where
Expand Down
10 changes: 5 additions & 5 deletions dhall/src/Dhall/Eval.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -437,7 +437,7 @@ eval !env t =
`vApp` VHLam (Typed "a" a) (\x ->
VHLam (Typed "as" (VList a)) (\as ->
vListAppend (VListLit Nothing (pure x)) as))
`vApp` VListLit (Just a) mempty
`vApp` VListLit (Just (VList a)) mempty

ListFold -> VPrim $ \a -> VPrim $ \case
VListLit _ as ->
Expand Down Expand Up @@ -465,8 +465,8 @@ eval !env t =
ListIndexed -> VPrim $ \ a -> VPrim $ \case
VListLit _ as -> let
a' = if null as then
Just (VRecord (Dhall.Map.fromList
[("index", VNatural), ("value", a)]))
Just (VList (VRecord (Dhall.Map.fromList
[("index", VNatural), ("value", a)])))
else
Nothing
as' = Data.Sequence.mapWithIndex
Expand Down Expand Up @@ -529,8 +529,8 @@ eval !env t =
| otherwise -> error errorMsg
(x, y, ma) -> VMerge x y ma
ToMap x ma -> case (evalE x, evalE <$> ma) of
(VRecordLit m, Just (VList t)) | null m ->
VListLit (Just t) (Data.Sequence.empty)
(VRecordLit m, ma'@(Just _)) | null m ->
VListLit ma' (Data.Sequence.empty)
(VRecordLit m, _) -> let
entry (k, v) =
VRecordLit (Dhall.Map.fromList [("mapKey", VTextLit $ VChunks [] k),
Expand Down
23 changes: 7 additions & 16 deletions dhall/src/Dhall/Parser/Expression.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,10 +77,6 @@ noted parser = do
Note src₁ _ | laxSrcEq src₀ src₁ -> return e
_ -> return (Note src₀ e)

shallowDenote :: Expr s a -> Expr s a
shallowDenote (Note _ e) = shallowDenote e
shallowDenote e = e

completeExpression :: Parser a -> Parser (Expr Src a)
completeExpression embedded = completeExpression_
where
Expand Down Expand Up @@ -181,18 +177,13 @@ parsers embedded = Parsers {..}

b <- expression

case (shallowDenote a, shallowDenote b) of
(ListLit _ xs, App f c) ->
case shallowDenote f of
List -> case xs of
[] -> return (ListLit (Just c) xs)
_ -> return (Annot a b)
_ ->
return (Annot a b)
(Merge c d _, e) ->
return (Merge c d (Just e))
(ToMap c _, d) ->
return (ToMap c (Just d))
case shallowDenote a of
ListLit _ [] ->
return (ListLit (Just b) [])
Merge c d _ ->
return (Merge c d (Just b))
ToMap c _ ->
return (ToMap c (Just b))
_ -> return (Annot a b)

alternative4A <|> alternative4B <|> pure a
Expand Down
2 changes: 1 addition & 1 deletion dhall/src/Dhall/Pretty/Internal.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -571,7 +571,7 @@ prettyCharacterSet characterSet expression =
prettyAnnotatedExpression (ListLit (Just a) b) =
list (map prettyExpression (Data.Foldable.toList b))
<> " : "
<> prettyApplicationExpression (App List a)
<> prettyApplicationExpression a
prettyAnnotatedExpression (Note _ a) =
prettyAnnotatedExpression a
prettyAnnotatedExpression a0 =
Expand Down
48 changes: 32 additions & 16 deletions dhall/src/Dhall/TypeCheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ typeWithA tpa = loop
s <- fmap Dhall.Core.normalize (loop ctx t)
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidListType t))
_ -> Left (TypeError ctx e (InvalidListType (App List t)))
flip traverseWithIndex_ xs' (\i x -> do
t' <- loop ctx x
if Dhall.Core.judgmentallyEqual t t'
Expand All @@ -387,20 +387,25 @@ typeWithA tpa = loop
Left (TypeError ctx x err) )
return (App List t)
_ -> Left (TypeError ctx e MissingListType)
loop ctx e@(ListLit (Just t ) xs) = do
s <- fmap Dhall.Core.normalize (loop ctx t)
case s of
Const Type -> return ()
_ -> Left (TypeError ctx e (InvalidListType t))
loop ctx e@(ListLit (Just t0) xs) = do
_ <- loop ctx t0
let nf_t0 = Dhall.Core.normalize t0
t1 <- case nf_t0 of
App List t1 -> do
s <- fmap Dhall.Core.normalize (loop ctx t1)
case s of
Const Type -> return t1
_ -> Left (TypeError ctx e (InvalidListType nf_t0))
_ -> Left (TypeError ctx e (InvalidListType nf_t0))
flip traverseWithIndex_ xs (\i x -> do
t' <- loop ctx x
if Dhall.Core.judgmentallyEqual t t'
if Dhall.Core.judgmentallyEqual t1 t'
then return ()
else do
let nf_t = Dhall.Core.normalize t
let nf_t = Dhall.Core.normalize t1
let nf_t' = Dhall.Core.normalize t'
Left (TypeError ctx x (InvalidListElement i nf_t x nf_t')) )
return (App List t)
return (App List t1)
loop ctx e@(ListAppend l r ) = do
tl <- fmap Dhall.Core.normalize (loop ctx l)
el <- case tl of
Expand Down Expand Up @@ -1874,11 +1879,11 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =

prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
where
short = "Invalid type for ❰List❱ elements"
short = "Invalid type for ❰List❱"

long =
"Explanation: ❰List❱s can optionally document the type of their elements with a \n\
\type annotation, like this: \n\
"Explanation: ❰List❱s can optionally document their type with a type annotation, \n\
\like this: \n\
\ \n\
\ \n\
\ ┌──────────────────────────┐ \n\
Expand All @@ -1892,8 +1897,19 @@ prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
\ ┌───────────────────┐ \n\
\ │ [] : List Natural │ An empty ❰List❱ \n\
\ └───────────────────┘ \n\
\ ⇧ \n\
\ You must specify the type when the ❰List❱ is empty \n\
\ ⇧ \n\
\ You must specify the type when the ❰List❱ is empty \n\
\ \n\
\ \n\
\The type must be of the form ❰List ...❱ and not something else. For example, \n\
\the following type annotation is " <> _NOT <> " valid: \n\
\ \n\
\ \n\
\ ┌────────────┐ \n\
\ │ ... : Bool │ \n\
\ └────────────┘ \n\
\ ⇧ \n\
\ This type does not have the form ❰List ...❱ \n\
\ \n\
\ \n\
\The element type must be a type and not something else. For example, the \n\
Expand All @@ -1914,11 +1930,11 @@ prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
\ This is a ❰Kind❱ and not a ❰Type❱ \n\
\ \n\
\ \n\
\You declared that the ❰List❱'s elements should have type: \n\
\You declared that the ❰List❱ should have type: \n\
\ \n\
\" <> txt0 <> "\n\
\ \n\
\... which is not a ❰Type❱ \n"
\... which is not a valid list type \n"
where
txt0 = insert expr0

Expand Down
16 changes: 14 additions & 2 deletions dhall/tests/Dhall/Test/Parser.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ import Prelude hiding (FilePath)
import Test.Tasty (TestTree)
import Turtle (FilePath, (</>))

import qualified Codec.CBOR.Read as CBOR
import qualified Codec.CBOR.Term as CBOR
import qualified Codec.Serialise as Serialise
import qualified Control.Monad as Monad
import qualified Data.ByteString as ByteString
Expand Down Expand Up @@ -74,6 +76,9 @@ getTests = do
-- The same performance improvements also broke the
-- precedence of parsing empty list literals
, parseDirectory </> "failure/unit/ListLitEmptyPrecedence.dhall"

-- https://github.com/dhall-lang/dhall-haskell/pull/1104
, parseDirectory </> "failure/nonCharacter.dhall"
]

Monad.guard (path `notElem` skip)
Expand Down Expand Up @@ -126,8 +131,15 @@ shouldParse path = do

let bytes = Serialise.serialise term

let message = "The expected CBOR representation doesn't match the actual one"
Tasty.HUnit.assertEqual message encoded bytes
Monad.unless (encoded == bytes) $ do
("", expected) <- Core.throws (CBOR.deserialiseFromBytes CBOR.decodeTerm encoded)

let message = "The expected CBOR representation doesn't match the actual one\n"
sjakobi marked this conversation as resolved.
Show resolved Hide resolved
++ "expected: " ++ show expected ++ "\n but got: " ++ show term
++ "\n expr: " ++ show expression

Tasty.HUnit.assertFailure message


shouldNotParse :: Text -> TestTree
shouldNotParse path = do
Expand Down