Rename Maybe to Optional
The primary reason for this change is to make it easier to describe these values
both in documentation and in informal communication between developers.
Before, you'd have to say things like:
* A value of type `Maybe` (incorrect)
* A `Maybe` value (sounds weird)
* A value of type `Maybe a` for some `a` (correct, but very verbose)
Now you can say an `Optional` value and the meaning is precise and clear
A secondary reason for this change is to keep the terminology close to the
intended use of the language for configuration files. Describing fields as
`Optional` instead of `Maybe` makes a lot of sense for configurations.
The disadvantage is that some uses of `Optional` don't make sense. For example,
consider the type of `List/head`:
List/head : ∀(a : Type) → List a → Optional a
It seems weird to say that the result of `List/head` is `Optional`. However,
many languages (such as Java/Scala/F#/Swift) already use this name or `Option` and
they get along just fine.
This commit is contained in:
Gabriel Gonzalez
parent
091b4cb36b
commit
7fe24bc8c4
|
|
@ -485,11 +485,11 @@ Nothing
|
|||
maybe :: Type a -> Type (Maybe a)
|
||||
maybe (Type extractIn expectedIn) = Type extractOut expectedOut
|
||||
where
|
||||
extractOut (MaybeLit _ es) = traverse extractIn es'
|
||||
extractOut (OptionalLit _ es) = traverse extractIn es'
|
||||
where
|
||||
es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)
|
||||
|
||||
expectedOut = App Maybe expectedIn
|
||||
expectedOut = App Optional expectedIn
|
||||
|
||||
{-| Decode a `Vector`
|
||||
|
||||
|
|
|
|||
|
|
@ -240,13 +240,13 @@ data Expr s a
|
|||
| ListIndexed
|
||||
-- | > ListReverse ~ List/reverse
|
||||
| ListReverse
|
||||
-- | > Maybe ~ Maybe
|
||||
| Maybe
|
||||
-- | > MaybeLit t [e] ~ [e] : Maybe t
|
||||
-- > MaybeLit t [] ~ [] : Maybe t
|
||||
| MaybeLit (Expr s a) (Vector (Expr s a))
|
||||
-- | > MaybeFold ~ Maybe/fold
|
||||
| MaybeFold
|
||||
-- | > Optional ~ Optional
|
||||
| Optional
|
||||
-- | > OptionalLit t [e] ~ [e] : Optional t
|
||||
-- > OptionalLit t [] ~ [] : Optional t
|
||||
| OptionalLit (Expr s a) (Vector (Expr s a))
|
||||
-- | > OptionalFold ~ Optional/fold
|
||||
| OptionalFold
|
||||
-- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }
|
||||
| Record (Map Text (Expr s a))
|
||||
-- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }
|
||||
|
|
@ -314,9 +314,9 @@ instance Monad (Expr s) where
|
|||
ListLast >>= _ = ListLast
|
||||
ListIndexed >>= _ = ListIndexed
|
||||
ListReverse >>= _ = ListReverse
|
||||
Maybe >>= _ = Maybe
|
||||
MaybeLit t es >>= k = MaybeLit (t >>= k) (fmap (>>= k) es)
|
||||
MaybeFold >>= _ = MaybeFold
|
||||
Optional >>= _ = Optional
|
||||
OptionalLit t es >>= k = OptionalLit (t >>= k) (fmap (>>= k) es)
|
||||
OptionalFold >>= _ = OptionalFold
|
||||
Record kts >>= k = Record (fmap (>>= k) kts)
|
||||
RecordLit kvs >>= k = RecordLit (fmap (>>= k) kvs)
|
||||
Union kts >>= k = Union (fmap (>>= k) kts)
|
||||
|
|
@ -367,9 +367,9 @@ instance Bifunctor Expr where
|
|||
first _ ListLast = ListLast
|
||||
first _ ListIndexed = ListIndexed
|
||||
first _ ListReverse = ListReverse
|
||||
first _ Maybe = Maybe
|
||||
first k (MaybeLit a b ) = MaybeLit (first k a) (fmap (first k) b)
|
||||
first _ MaybeFold = MaybeFold
|
||||
first _ Optional = Optional
|
||||
first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b)
|
||||
first _ OptionalFold = OptionalFold
|
||||
first k (Record a ) = Record (fmap (first k) a)
|
||||
first k (RecordLit a ) = RecordLit (fmap (first k) a)
|
||||
first k (Union a ) = Union (fmap (first k) a)
|
||||
|
|
@ -471,24 +471,10 @@ buildExpr1 (Let a (Just b) c d) =
|
|||
<> buildExpr0 c
|
||||
<> " in "
|
||||
<> buildExpr1 d
|
||||
-- Note: The corresponding @Expr1@ parser in "Dhall.Parser" deviates from the
|
||||
-- following two cases due to the fact that the @alex@-generated parser does not
|
||||
-- not backtrack perfectly. The exact translation would be:
|
||||
--
|
||||
-- > Expr1
|
||||
-- > ...
|
||||
-- > | '[' Elems ']' : 'List' Expr6
|
||||
-- > { ListLit $6 (Data.Vector.fromList $2) }
|
||||
-- > | '[' Elems ']' : 'Maybe' Expr6
|
||||
-- > { MaybeLit $6 (Data.Vector.fromList $2) }
|
||||
--
|
||||
-- ... but that fails to parse @Maybe@ literals correctly, so I worked around
|
||||
-- it by changing the parser to an equivalent parser but keeping the
|
||||
-- builder the same.
|
||||
buildExpr1 (ListLit a b) =
|
||||
"[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExpr6 a
|
||||
buildExpr1 (MaybeLit a b) =
|
||||
"[" <> buildElems (Data.Vector.toList b) <> "] : Maybe " <> buildExpr6 a
|
||||
buildExpr1 (OptionalLit a b) =
|
||||
"[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExpr6 a
|
||||
buildExpr1 (Merge a b c) =
|
||||
"apply " <> buildExpr6 a <> " " <> buildExpr6 b <> " : " <> buildExpr5 c
|
||||
buildExpr1 (Note _ b) =
|
||||
|
|
@ -567,10 +553,10 @@ buildExpr6 ListIndexed =
|
|||
"List/indexed"
|
||||
buildExpr6 ListReverse =
|
||||
"List/reverse"
|
||||
buildExpr6 Maybe =
|
||||
"Maybe"
|
||||
buildExpr6 MaybeFold =
|
||||
"Maybe/fold"
|
||||
buildExpr6 Optional =
|
||||
"Optional"
|
||||
buildExpr6 OptionalFold =
|
||||
"Optional/fold"
|
||||
buildExpr6 (BoolLit True) =
|
||||
"True"
|
||||
buildExpr6 (BoolLit False) =
|
||||
|
|
@ -847,12 +833,12 @@ shift _ _ ListHead = ListHead
|
|||
shift _ _ ListLast = ListLast
|
||||
shift _ _ ListIndexed = ListIndexed
|
||||
shift _ _ ListReverse = ListReverse
|
||||
shift _ _ Maybe = Maybe
|
||||
shift d v (MaybeLit a b) = MaybeLit a' b'
|
||||
shift _ _ Optional = Optional
|
||||
shift d v (OptionalLit a b) = OptionalLit a' b'
|
||||
where
|
||||
a' = shift d v a
|
||||
b' = fmap (shift d v) b
|
||||
shift _ _ MaybeFold = MaybeFold
|
||||
shift _ _ OptionalFold = OptionalFold
|
||||
shift d v (Record a) = Record a'
|
||||
where
|
||||
a' = fmap (shift d v) a
|
||||
|
|
@ -978,12 +964,12 @@ subst _ _ ListHead = ListHead
|
|||
subst _ _ ListLast = ListLast
|
||||
subst _ _ ListIndexed = ListIndexed
|
||||
subst _ _ ListReverse = ListReverse
|
||||
subst _ _ Maybe = Maybe
|
||||
subst x e (MaybeLit a b) = MaybeLit a' b'
|
||||
subst _ _ Optional = Optional
|
||||
subst x e (OptionalLit a b) = OptionalLit a' b'
|
||||
where
|
||||
a' = subst x e a
|
||||
b' = fmap (subst x e) b
|
||||
subst _ _ MaybeFold = MaybeFold
|
||||
subst _ _ OptionalFold = OptionalFold
|
||||
subst x e (Record kts) = Record (fmap (subst x e) kts)
|
||||
subst x e (RecordLit kvs) = RecordLit (fmap (subst x e) kvs)
|
||||
subst x e (Union kts) = Union (fmap (subst x e) kts)
|
||||
|
|
@ -1092,9 +1078,9 @@ normalize e = case e of
|
|||
App (App ListLength _) (ListLit _ ys) ->
|
||||
NaturalLit (fromIntegral (Data.Vector.length ys))
|
||||
App (App ListHead _) (ListLit t ys) ->
|
||||
normalize (MaybeLit t (Data.Vector.take 1 ys))
|
||||
normalize (OptionalLit t (Data.Vector.take 1 ys))
|
||||
App (App ListLast _) (ListLit t ys) ->
|
||||
normalize (MaybeLit t y)
|
||||
normalize (OptionalLit t y)
|
||||
where
|
||||
y = if Data.Vector.null ys
|
||||
then Data.Vector.empty
|
||||
|
|
@ -1114,7 +1100,7 @@ normalize e = case e of
|
|||
]
|
||||
App (App ListReverse _) (ListLit t xs) ->
|
||||
normalize (ListLit t (Data.Vector.reverse xs))
|
||||
App (App (App (App (App MaybeFold _) (MaybeLit _ xs)) _) just) nothing ->
|
||||
App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->
|
||||
normalize (maybe nothing just' (toMaybe xs))
|
||||
where
|
||||
just' y = App just y
|
||||
|
|
@ -1232,12 +1218,12 @@ normalize e = case e of
|
|||
ListLast -> ListLast
|
||||
ListIndexed -> ListIndexed
|
||||
ListReverse -> ListReverse
|
||||
Maybe -> Maybe
|
||||
MaybeLit t es -> MaybeLit t' es'
|
||||
Optional -> Optional
|
||||
OptionalLit t es -> OptionalLit t' es'
|
||||
where
|
||||
t' = normalize t
|
||||
es' = fmap normalize es
|
||||
MaybeFold -> MaybeFold
|
||||
OptionalFold -> OptionalFold
|
||||
Record kts -> Record kts'
|
||||
where
|
||||
kts' = fmap normalize kts
|
||||
|
|
|
|||
|
|
@ -138,8 +138,8 @@ identifierStyle = IdentifierStyle
|
|||
, "List/last"
|
||||
, "List/indexed"
|
||||
, "List/reverse"
|
||||
, "Maybe"
|
||||
, "Maybe/fold"
|
||||
, "Optional"
|
||||
, "Optional/fold"
|
||||
]
|
||||
, _styleHighlight = Identifier
|
||||
, _styleReservedHighlight = ReservedIdentifier
|
||||
|
|
@ -280,8 +280,8 @@ listLike =
|
|||
return ListLit
|
||||
|
||||
listLike1 = do
|
||||
reserve "Maybe"
|
||||
return MaybeLit
|
||||
reserve "Optional"
|
||||
return OptionalLit
|
||||
|
||||
-- TODO: Add `noted` in the right places here
|
||||
exprC :: Parser (Expr Src Path)
|
||||
|
|
@ -451,12 +451,12 @@ exprF = choice
|
|||
return ListReverse
|
||||
|
||||
exprF19 = do
|
||||
reserve "Maybe"
|
||||
return Maybe
|
||||
reserve "Optional"
|
||||
return Optional
|
||||
|
||||
exprF20 = do
|
||||
reserve "Maybe/fold"
|
||||
return MaybeFold
|
||||
reserve "Optional/fold"
|
||||
return OptionalFold
|
||||
|
||||
exprF21 = do
|
||||
reserve "Bool"
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ propEqual eL0 eR0 =
|
|||
go Double Double = return True
|
||||
go Text Text = return True
|
||||
go List List = return True
|
||||
go Maybe Maybe = return True
|
||||
go Optional Optional = return True
|
||||
go (Record ktsL0) (Record ktsR0) = do
|
||||
let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
|
||||
| kL == kR = do
|
||||
|
|
@ -359,9 +359,9 @@ typeWith _ ListFold = do
|
|||
typeWith _ ListLength = do
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") Natural))
|
||||
typeWith _ ListHead = do
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Maybe "a")))
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a")))
|
||||
typeWith _ ListLast = do
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Maybe "a")))
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a")))
|
||||
typeWith _ ListIndexed = do
|
||||
let kts = [("index", Natural), ("value", "a")]
|
||||
return
|
||||
|
|
@ -370,16 +370,16 @@ typeWith _ ListIndexed = do
|
|||
(App List (Record (Data.Map.fromList kts))) ) )
|
||||
typeWith _ ListReverse = do
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a")))
|
||||
typeWith _ Maybe = do
|
||||
typeWith _ Optional = do
|
||||
return (Pi "_" (Const Type) (Const Type))
|
||||
typeWith ctx e@(MaybeLit t xs ) = do
|
||||
typeWith ctx e@(OptionalLit t xs) = do
|
||||
s <- fmap Dhall.Core.normalize (typeWith ctx t)
|
||||
case s of
|
||||
Const Type -> return ()
|
||||
_ -> Left (TypeError ctx e (InvalidMaybeType t))
|
||||
_ -> Left (TypeError ctx e (InvalidOptionalType t))
|
||||
let n = Data.Vector.length xs
|
||||
if 2 <= n
|
||||
then Left (TypeError ctx e (InvalidMaybeLiteral n))
|
||||
then Left (TypeError ctx e (InvalidOptionalLiteral n))
|
||||
else return ()
|
||||
forM_ xs (\x -> do
|
||||
t' <- typeWith ctx x
|
||||
|
|
@ -388,12 +388,12 @@ typeWith ctx e@(MaybeLit t xs ) = do
|
|||
else do
|
||||
let nf_t = Dhall.Core.normalize t
|
||||
let nf_t' = Dhall.Core.normalize t'
|
||||
Left (TypeError ctx e (InvalidMaybeElement x nf_t nf_t')) )
|
||||
return (App Maybe t)
|
||||
typeWith _ MaybeFold = do
|
||||
Left (TypeError ctx e (InvalidOptionalElement x nf_t nf_t')) )
|
||||
return (App Optional t)
|
||||
typeWith _ OptionalFold = do
|
||||
return
|
||||
(Pi "a" (Const Type)
|
||||
(Pi "_" (App Maybe "a")
|
||||
(Pi "_" (App Optional "a")
|
||||
(Pi "maybe" (Const Type)
|
||||
(Pi "just" (Pi "_" "a" "maybe")
|
||||
(Pi "nothing" "maybe" "maybe") ) ) ) )
|
||||
|
|
@ -520,9 +520,9 @@ data TypeMessage s
|
|||
| Untyped
|
||||
| InvalidListElement Int (Expr s X) (Expr s X) (Expr s X)
|
||||
| InvalidListType (Expr s X)
|
||||
| InvalidMaybeElement (Expr s X) (Expr s X) (Expr s X)
|
||||
| InvalidMaybeLiteral Int
|
||||
| InvalidMaybeType (Expr s X)
|
||||
| InvalidOptionalElement (Expr s X) (Expr s X) (Expr s X)
|
||||
| InvalidOptionalLiteral Int
|
||||
| InvalidOptionalType (Expr s X)
|
||||
| InvalidPredicate (Expr s X) (Expr s X)
|
||||
| IfBranchMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)
|
||||
| IfBranchMustBeTerm Bool (Expr s X) (Expr s X) (Expr s X)
|
||||
|
|
@ -890,22 +890,22 @@ the following expressions are all functions because they have a function type:
|
|||
The function's output kind is ❮Type❯
|
||||
|
||||
|
||||
The function's input kind is ❮Type❯
|
||||
Function's input has kind ❮Type❯
|
||||
⇩
|
||||
┌──────────────────────────────────────────────┐
|
||||
│ List/head : ∀(a : Type) → (List a → Maybe a) │ A function can return
|
||||
└──────────────────────────────────────────────┘ another function
|
||||
┌─────────────────────────────────────────────────┐
|
||||
│ List/head : ∀(a : Type) → (List a → Optional a) │ A function can return
|
||||
└─────────────────────────────────────────────────┘ another function
|
||||
⇧
|
||||
The function's output type is ❮List a → Maybe a❯
|
||||
Function's output has type ❮List a → Optional a❯
|
||||
|
||||
|
||||
The function's input type is ❮List Text❯
|
||||
⇩
|
||||
┌─────────────────────────────────────────┐
|
||||
│ List/head Text : List Text → Maybe Text │ A function applied to an
|
||||
└─────────────────────────────────────────┘ argument can be a function
|
||||
┌────────────────────────────────────────────┐
|
||||
│ List/head Text : List Text → Optional Text │ A function applied to an
|
||||
└────────────────────────────────────────────┘ argument can be a function
|
||||
⇧
|
||||
The function's output type is ❮Maybe Text❯
|
||||
The function's output type is ❮Optional Text❯
|
||||
|
||||
|
||||
An expression is not a function if the expression's type is not of the form
|
||||
|
|
@ -1529,40 +1529,40 @@ Your list elements should have this type:
|
|||
txt2 = Text.toStrict (Dhall.Core.pretty expr1)
|
||||
txt3 = Text.toStrict (Dhall.Core.pretty expr2)
|
||||
|
||||
prettyTypeMessage (InvalidMaybeType expr0) = ErrorMessages {..}
|
||||
prettyTypeMessage (InvalidOptionalType expr0) = ErrorMessages {..}
|
||||
where
|
||||
short = "Invalid type for ❮Maybe❯ elements"
|
||||
short = "Invalid type for ❮Optional❯ elements"
|
||||
|
||||
long =
|
||||
Builder.fromText [NeatInterpolation.text|
|
||||
Explanation: Every optional value ends with a type annotation for the element
|
||||
that might be stored inside. For example, these are valid expressions:
|
||||
|
||||
[1] : Maybe Integer -- An optional value that's present
|
||||
[] : Maybe Integer -- An optional value that's absent
|
||||
[1] : Optional Integer -- An optional value that's present
|
||||
[] : Optional Integer -- An optional value that's absent
|
||||
|
||||
The type following the `Maybe` is the "type parameter", and must be a type:
|
||||
The type following the `Optional` is the "type parameter", and must be a type:
|
||||
|
||||
Maybe Integer -- This is valid, because `Integer` is a type
|
||||
Maybe Text -- This is also valid, because `Text` is a type
|
||||
Optional Integer -- This is valid, because `Integer` is a type
|
||||
Optional Text -- This is also valid, because `Text` is a type
|
||||
|
||||
... but the type parameter must *not* be a term or kind:
|
||||
|
||||
Maybe 1 -- This is invalid, because `1` is a term
|
||||
Maybe Type -- This is invalid, because `Type` is a kind
|
||||
Optional 1 -- This is invalid, because `1` is a term
|
||||
Optional Type -- This is invalid, because `Type` is a kind
|
||||
|
||||
You provided a type parameter for the `Maybe` that is not a valid type:
|
||||
You provided a type parameter for the `Optional` that is not a valid type:
|
||||
|
||||
$insert
|
||||
|]
|
||||
where
|
||||
txt0 = Text.toStrict (Builder.toLazyText (Dhall.Core.buildExpr6 expr0))
|
||||
insert = indent [NeatInterpolation.text|
|
||||
[ ... ] : Maybe $txt0
|
||||
[ ... ] : Optional $txt0
|
||||
-- ^ This needs to be a type
|
||||
|]
|
||||
|
||||
prettyTypeMessage (InvalidMaybeElement expr0 expr1 expr2) = ErrorMessages {..}
|
||||
prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..}
|
||||
where
|
||||
short = "Optional expression with an element of the wrong type"
|
||||
|
||||
|
|
@ -1571,11 +1571,11 @@ prettyTypeMessage (InvalidMaybeElement expr0 expr1 expr2) = ErrorMessages {..}
|
|||
Explanation: An optional value that is present must have a type matching the
|
||||
corresponding type annotation. For example, this is a valid optional value:
|
||||
|
||||
[1] : Maybe Integer -- The type of `1` is `Integer`, which matches
|
||||
[1] : Optional Integer -- The type of `1` is `Integer`, which matches
|
||||
|
||||
... but this is *not* a valid optional value:
|
||||
|
||||
[1] : Maybe Text -- Invalid, because the type of `1` is not `Text`
|
||||
[1] : Optional Text -- Invalid, because the type of `1` is not `Text`
|
||||
|
||||
Your optional value has a type which does not match the type annotation:
|
||||
|
||||
|
|
@ -1591,11 +1591,11 @@ The element you provided actually has this type:
|
|||
insert = indent [NeatInterpolation.text|
|
||||
[ $txt0
|
||||
-- ^ This value ...
|
||||
] : Maybe $txt1
|
||||
-- ^ ... needs to have a type matching this type parameter
|
||||
] : Optional $txt1
|
||||
-- ^ ... needs to have a type matching this type parameter
|
||||
|]
|
||||
|
||||
prettyTypeMessage (InvalidMaybeLiteral n) = ErrorMessages {..}
|
||||
prettyTypeMessage (InvalidOptionalLiteral n) = ErrorMessages {..}
|
||||
where
|
||||
short = "More than one element for an optional value"
|
||||
|
||||
|
|
@ -1604,16 +1604,16 @@ prettyTypeMessage (InvalidMaybeLiteral n) = ErrorMessages {..}
|
|||
Explanation: The syntax for an optional value resembles the syntax for `List`
|
||||
literals:
|
||||
|
||||
[] : Maybe Integer -- A valid literal for an absent optional value
|
||||
[1] : Maybe Integer -- A valid literal for a present optional value
|
||||
[] : List Integer -- A valid literal for an empty (0-element) `List`
|
||||
[1] : List Integer -- A valid literal for a singleton (1-element) `List`
|
||||
[] : Optional Integer -- A valid literal for an absent optional value
|
||||
[1] : Optional Integer -- A valid literal for a present optional value
|
||||
[] : List Integer -- A valid literal for an empty (0-element) `List`
|
||||
[1] : List Integer -- A valid literal for a singleton (1-element) `List`
|
||||
|
||||
However, an optional value can *not* have more than one element, whereas a
|
||||
`List` can have multiple elements:
|
||||
|
||||
[1, 2] : Maybe Integer -- Invalid: multiple elements not allowed
|
||||
[1, 2] : List Integer -- Valid : multiple elements allowed
|
||||
[1, 2] : Optional Integer -- Invalid: multiple elements not allowed
|
||||
[1, 2] : List Integer -- Valid : multiple elements allowed
|
||||
|
||||
Your optional value had $txt0 elements, which is not allowed. Optional values
|
||||
can only have at most one element
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user