A few updates to builtin notes #4659
Conversation
There was a problem hiding this comment.
OK, clearly the original wording was too confusing. However the new one has a lot of problems too.
I now believe this whole explanation about how (a, b) is troubling should be moved elsewhere and elaborated on properly, with the full horrible details. I thought I could get away with describing the problems quickly here, but I clearly failed, and blowing up these important high-level docs with so low-level details of what we can't do isn't really appropriate.
So let me propose the following: I'll create for myself a task for the next sprint to properly document this particular problem and assign you as a reviewer once I'm done.
I'll also fix my inconsistent usage of the "unlift" term.
Sounds fine?
| When it comes to polymorphic types, unlifting a @val@ into an @Opaque val a@ is trivial - it's just | ||
| @makeKnown@. However, there's no sensible way of unlifting a @val@ into, say, @[Opaque val a]@ |
There was a problem hiding this comment.
makeKnown is an implementation detail and doesn't belong to this file. The file doesn't have any mentions of readKnown, makeKnown, ReadKnownIn, MakeKnownIn, KnownTypeAst etc. Plus, all of that gets optimized away and doesn't appear in the generated Core for builtins, so those are just some intermediate auxiliary abstractions and we shouldn't pollute the high-level description of the built-in functions machinery with them.
And the fact that it's just makeKnown doesn't tell the reader much anyway: we are talking about theoretic limitations here, we could've implemented the slow version and unlift a val as a list and it also would be makeKnown.
... except not makeKnown, which is normally for lifting, but readKnown, which is normally for unlifting. It's just that if go with unlifting to [Opaque val a], we have to do lifting during unlifting. We don't do that anywhere in our instances, but for that [Opaque val a] we'd have to. The opposite is also true: we have to do unlifting during lifting of an [Opaque val a].
We also never lift to or unlift from a val, it's always Opaque val a.
The original wording of these two lines was more precise: it was saying that we couldn't do something for any [a] when a is not a builtin. In your version it's not clear if it's specific to Opaque or not (for example, if SomeConstant is OK unlike Opaque).
I'm not trying to overwhelm you with criticism or something, just clarifying. I appreciate you rewording the original version, clearly it was confusing (especially the part where my usages of "unlifting" are wildly inconsistent), but we'll need to come up with a more fitting rewording.
| unlifting is supposed to be cheap, while mapping over a list is O(n). This isn't a problem for | ||
| @NullList@ because it only needs to examine whether the list is empty, but it is a problem for @MkCons@ |
There was a problem hiding this comment.
No, that's the whole point! NullList is as problematic as MkCons in that regard. It doesn't matter if a built-in function consumes a list or produces one, if that involves any [Opaque val a], we have to use a map and this is where the linearity comes from.
There was a problem hiding this comment.
How so, if we never need the elements of the list? Like null . map f is O(1) just like null is?
There was a problem hiding this comment.
Just to record what we discussed during our call:
- I meant
traverserather thanmaplike here (where we don't havetraverse, but unlift each element of a tuple using the monadicreadKnown, which is the tuples analogue) - but I was wrong about that, we don't need
readKnownand can simply useOpaque . fromConstant, then we can usemapandnull . map fis indeed O(1) - however that only works for lazy data types and it would be very weird if lazy built-in types were fine and strict ones -- an order of magnitude slower
| nullList :: [a] -> Bool | ||
| (:) :: a -> [a] -> [a] |
There was a problem hiding this comment.
I shouldn't have mentioned MkCons above. While NullList and MkCons are equally problematic w.r.t. linearity, they are not equally problematic w.r.t. required expressiveness. If didn't care about performance or employed some clever way of working around the performance problems, we would be able to define NullList, but not MkCons, because the latter has to check two type tags coming from arguments for equality, while the former only needs to look at the head of a single type tag (we used to do that, but it was too slow, so it was removed. We never supported automatic handling of functions like MkCons, because that would be really complex).
| Note that this only applies when each unconstrained type variable is only used as the entire | ||
| type of one or more arguments, as is the case with @\b x y -> if b then x else y@. Otherwise, |
There was a problem hiding this comment.
That's not true. It's fine to apply EvaluationResult or Emitter or Opaque or any combination of those to a type variable.
There was a problem hiding this comment.
No need to fix anything in the doc immediately; I don't think it's high priority but feel free to do so. Even reading a peer-reviewed publication it's normal to misunderstand some parts especially if the topic is complex and unfamiliar - not failed or bad documentation at all. And trying to rephrase something is a great way to see if I'm really understanding it correctly.
| unlifting is supposed to be cheap, while mapping over a list is O(n). This isn't a problem for | ||
| @NullList@ because it only needs to examine whether the list is empty, but it is a problem for @MkCons@ |
There was a problem hiding this comment.
How so, if we never need the elements of the list? Like null . map f is O(1) just like null is?
I went through the builtin notes (great docs by the way) and made a few small changes which would have made things clearer for myself.