-
Notifications
You must be signed in to change notification settings - Fork 213
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.
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
Fix semantics of {List,Optional,Natural}/build
#300
Conversation
This fixes all of the build built-ins to match the standard semantics The easiest way to illustrate the problem is the following example from the test suite: ```haskell λ(id : ∀(a : Type) → a → a) → Natural/build ( λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → id natural (succ zero) ) ``` According to the standard semantics that should normalize to: ```haskell λ(id : ∀(a : Type) → a → a) → id Natural +1 ``` ... but before this change it was not reducing at all. After this change it reduces correctly. However, there is a further issue, which is that correctly implementing the semantics leads to poor time complexity for `List/build` since it is specified in terms of repeatedly prepending a single element, which leads to quadratic time complexity since lists are implemented in terms of `Vector` under the hood. You might think that you could use the efficient approach for expressions like this: ```haskell List/build Bool ( λ(list : Type) → λ(cons : Bool → list → list) → λ(nil : list) → cons True (cons False nil) ) ``` ... and then fall back on the slower approach for more interesting cases such as this: ```haskell λ(id : ∀(a : Type) → a → a) → List/build Bool ( λ(list : Type) → λ(cons : Bool → list → list) → λ(nil : list) → id list (cons True (cons False nil)) ) ``` ... but that does not work either! The reason why is that very often you don't use `List/build` directly and instead use it indirectly via helper functions such as `Prelude/List/concat`: ```haskell let concat : ∀(a : Type) → List (List a) → List a = λ(a : Type) → λ(xss : List (List a)) → List/build a ( λ(list : Type) → λ(cons : a → list → list) → λ(nil : list) → List/fold (List a) xss list ( λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys ) nil ) in concat ``` ... so what happens is that if you try to normalize something like: ```haskell concat Text [["Example"]] ``` ... the `concat` function will be normalized first, which will cause the `List/build` to be normalized when its argument is still abstract, which will trigger the slow path for the semantics. Consequently, this change also modifies Dhall lists to be backed by `Data.Sequence.Seq` instead of `Data.Vector.Vector`, so that `List/build` can always use the correct implementation of semantics in linear time while still implementing other operations on lists reasonably efficiently. This in turn triggers another change to the `OptionalLit` constructor to use `Maybe` to store the payload instead of `Vector`. The only reason that `OptionalLit` originally used `Vector` was so that `List/head` and `List/last` could be implemented as just a slice into the `ListLit` vector, but now that it's not a vector any longer it's simpler to just use a more accurate `Maybe` type to represent the payload.
[1,2,3] | ||
-} | ||
vector :: Type a -> Type (Vector a) | ||
vector (Type extractIn expectedIn) = Type extractOut expectedOut |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You could still keep this Type
and add sequence
. Takes one breaking change out.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's still present (see export list), but I just relocated it below so that they were in logical order (i.e. sequence
is the most direct one and then list
is defined in terms of sequence
and vector
is defined in terms of list
)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah cool, thanks!
This fixes all of the build built-ins to match the standard semantics
The easiest way to illustrate the problem is the following example from
the test suite:
According to the standard semantics that should normalize to:
... but before this change it was not reducing at all. After this
change it reduces correctly.
However, there is a further issue, which is that correctly implementing
the semantics leads to poor time complexity for
List/build
since it isspecified in terms of repeatedly prepending a single element, which
leads to quadratic time complexity since lists are implemented in terms
of
Vector
under the hood.You might think that you could use the efficient approach for
expressions like this:
... and then fall back on the slower approach for more interesting cases
such as this:
... but that does not work either! The reason why is that very often
you don't use
List/build
directly and instead use it indirectly viahelper functions such as
Prelude/List/concat
:... so what happens is that if you try to normalize something like:
... the
concat
function will be normalized first, which will cause theList/build
to be normalized when its argument is still abstract, which willtrigger the slow path for the semantics.
Consequently, this change also modifies Dhall lists to be backed by
Data.Sequence.Seq
instead ofData.Vector.Vector
, so thatList/build
can always use the correct implementation of semanticsin linear time while still implementing other operations on lists
reasonably efficiently.
This in turn triggers another change to the
OptionalLit
constructorto use
Maybe
to store the payload instead ofVector
. The onlyreason that
OptionalLit
originally usedVector
was so thatList/head
andList/last
could be implemented as just a slice intothe
ListLit
vector, but now that it's not a vector any longer it'ssimpler to just use a more accurate
Maybe
type to represent thepayload.