[Builtins] Disentangle 'KnownTypeAst' from 'KnownTypeIn' #4312
Conversation
|
/benchmark |
|
Comparing benchmark results of 'c876b1530' (base) and 'c1beb8a0b' (PR)
|
effectfully
force-pushed
the
effectfully/disentangle-KnownTypeAst-from-KnownTypeIn
branch
from
889e799 to
20fd9d8
Compare
|
/benchmark |
|
Comparing benchmark results of 'c876b1530' (base) and '20fd9d80e' (PR)
|
|
/benchmark |
|
Comparing benchmark results of 'c876b1530' (base) and '4693b29bf' (PR)
|
|
/benchmark |
|
Comparing benchmark results of 'c876b1530' (base) and 'c42a9f252' (PR)
|
|
/benchmark |
|
Comparing benchmark results of 'c876b1530' (base) and '7d3c855f4' (PR)
|
| (Prelude.id | ||
| :: a ~ Opaque term (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer) | ||
| => a -> a) | ||
| (Prelude.id :: fi ~ Opaque term (TyAppRep f Integer) => fi -> fi) |
There was a problem hiding this comment.
The inference machinery now is able to look under TyAppRep
| (Prelude.id | ||
| :: a ~ Opaque term (PlcListRep (TyVarRep ('TyNameRep "a" 0))) | ||
| => a -> a) | ||
| (Prelude.id :: la ~ Opaque term (PlcListRep a) => la -> la) |
There was a problem hiding this comment.
and basically any
| :: ( f ~ 'TyNameRep "f" 0 | ||
| , a ~ 'TyNameRep @GHC.Type "a" 1 | ||
| , afa ~ Opaque term (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a))) | ||
| ) | ||
| :: afa ~ Opaque term (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a))) |
| -> SomeConstantPoly uni (,) '[a, b] | ||
| -> SomeConstant uni (a, b) |
There was a problem hiding this comment.
Quite nicer, isn't it?
There was a problem hiding this comment.
The rest of the file does look quite a bit more readable.
| -- >>> :t enumerateDebug $ Just 'a' | ||
| -- enumerateDebug $ Just 'a' :: Maybe Char |
There was a problem hiding this comment.
Had to drop it, 'cause it now generates a ton of garbage instead of being stuck. I'll work on it some time later.
| -- This constraint is just to get through 'KnownPolytype' stuck on an unknown type straight | ||
| -- to the custom type error that we have in the @Typed@ module. Though, somehow, the error | ||
| -- gets triggered even without the constraint when this function in used, but I don't | ||
| -- understand how that is possible and it does not work when the function from the @Debug@ | ||
| -- module is used. So we're just doing the right thing here and adding the constraint. | ||
| , KnownMonotype term args res a |
There was a problem hiding this comment.
This was used to trigger the now-dropped custom type error.
| -- Try to unify @a@ with a freshly created @var@. | ||
| , a ~?~ var | ||
| -- If @a@ is equal to @var@ then unification was successful and we just used the fresh id and | ||
| -- so we need to bump it up. Otherwise @var@ was discarded and so the fresh id is still fresh. | ||
| -- Replacing @(===)@ with @(==)@ causes errors at use site, for whatever reason. | ||
| , j ~ If (a === var) (i + 1) i | ||
| ) => TrySpecializeAsVar i j term a | ||
|
|
||
| -- | For looking under special-case types, for example the type of a constant or the type arguments |
There was a problem hiding this comment.
master:
this branch:
| -- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can | ||
| -- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@). | ||
| type SpecializeFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint | ||
| type SpecializeFromTo i j term a = HandleHole i j term (TypeHole a) |
There was a problem hiding this comment.
@michaelpj renamed EnumerateFromTo to SpecializeFromTo as requested.
| @@ -457,39 +457,163 @@ type HasConstant term = (AsConstant term, FromConstant term) | |||
| -- and connects @term@ and its @uni@. | |||
| type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term) | |||
|
|
|||
| {- Note [Rep vs Type context] | |||
There was a problem hiding this comment.
There has always been the distinction, but I'm only documenting it now.
| (fun (con integer) (fun [ (con list) (con data) ] (con data))) |
There was a problem hiding this comment.
This diff represents what the PR changes. Now we handle built-in types the same way regardless of whether they're fully monomorphized or not. Previously we had to distinguish between the two cases manually by choosing either SomeConstant or SomeConstantPoly when defining a builtin and now things are just consistent.
There was a problem hiding this comment.
s/monomorphized/normalized?
There was a problem hiding this comment.
No:
- we had to distinguish based on monomorphization happening or not, that's what my comment is about
- this type appears normalized only because
ElaborateBuiltinessentially performs normalization for built-in types. Any non built-in type would not be normalized. Again, we don't haveTyLamRepcurrently, but it's trivial to add it and then we could apply it usingTyAppRepand that wouldn't get normalized
There was a problem hiding this comment.
we had to distinguish based on monomorphization happening or not, that's what my comment is about
Well, we actually still have to, just in a different place. Writing a note.
|
This is another attempt at better API for polymorphic built-in functions over polymorphic built-in types. Based on #4220, but is more powerful and a lot simpler. I believe it's even simpler than what's in I think this concludes the API changes that I wanted to happen, now the interface for defining built-in functions should be stable (but the internals will change drastically if we're lucky). I'll be thinking how to explain builtins without committing too much to a particular representation of the internals. Ready for review. |
| type GetName :: GHC.Type -> Nat -> Symbol | ||
| type family GetName k i where | ||
| GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"] | ||
| GetName _ i = Lookup i '["f", "g", "h", "m", "n"] |
There was a problem hiding this comment.
worth a comment. This is intended for higher-kinded things, I assume.
| So instead of mixing up types whose values are actually unliftable with types that are only used | ||
| for type checking, we keep the distinction explicit. | ||
|
|
||
| The barrier between Haskell and Plutus is the barrier between the Type and the Rep contexts and |
There was a problem hiding this comment.
What if we view this through the lens we've talked about for the formalization: i.e. this distinction is rather one of kinds.
I'm not sure I've worked out how we might do it, but could we end up with something like this, where the user would write:
id :: forall (a :: ArbitraryType) . a -> a
idList :: forall (a :: BuiltinType) . [a] -> [a]
and then that works out? I know we don't have this distinction on the PLC side, but maybe we could have it here. Probably the devil is in the details, I don't know how we would implement that...
There was a problem hiding this comment.
idList :: forall (a :: BuiltinType) . [a] -> [a]
We can't have that, I'll add a note.
There was a problem hiding this comment.
Also [] has kind * -> *.
|
|
||
| The barrier between Haskell and Plutus is the barrier between the Type and the Rep contexts and | ||
| that barrier must always be some explicit type constructor that switches the context from Type to | ||
| Rep. We've only considered 'Opaque' as an example of such type constructor, but we also have |
There was a problem hiding this comment.
Opaque :: BuiltinType -> ArbitraryType?
There was a problem hiding this comment.
Opaque works in the opposite direction! It takes a representation of a Plutus type (so it may have type-level lambdas for example, although we don't provide them currently, but we provide TyForallRep, which is very similar) and constructs a liftable/unliftable type out of that. And in most cases Opaque is indexed by a type representing a Plutus type variable, so it's not about built-in types at all.
| (fun (con integer) (fun [ (con list) (con data) ] (con data))) |
There was a problem hiding this comment.
s/monomorphized/normalized?
|
Comments addressed, make sure to read another scary Note (as if we didn't have enough of them). |
Eek! Can you give some idea of how much more expressive it is? I'm worrying about specification here, and also maybe costing. In the specification I'm not trying to explain what's going on here, but rather what sort of things you're allowed to write, and with a generic description of the semantics of possible built-in functions and types. That's already quite difficult and it might be extremely hard to specify what's going on here in full generality. For example, I think you said that we could already implement GADTs if we wanted to, and as far as I can tell from Googling it's quite challenging to say what the semantics of those are. I suppose that there will be many things be that we might not want to allow as builtins for all kinds of reasons, like costing. For example, we can't allow |
| (all f (fun (type) (type)) (fun (all b (type) [ f b ]) (all b (type) [ f b ]))) |
There was a problem hiding this comment.
I guess that there will have been an a here that's disappeared during normalisation or something?
There was a problem hiding this comment.
It just got renamed to b. Previously we'd provide all the names manually, but now they get generated automatically and I didn't care enough to make the generated names look good in the higher-kinded case, 'cause we don't have that in the default builtins.
| -> SomeConstantPoly uni (,) '[a, b] | ||
| -> SomeConstant uni (a, b) |
There was a problem hiding this comment.
The rest of the file does look quite a bit more readable.
| type GetName i = Lookup i '["a", "b", "c", "d", "e", "f", "g", "h"] | ||
| type GetName :: GHC.Type -> Nat -> Symbol | ||
| type family GetName k i where | ||
| GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"] |
There was a problem hiding this comment.
Does the limited length of these lists imply a limit on the complexity of the types we can have, or is this just a cosmetic thing?
There was a problem hiding this comment.
Does the limited length of these lists imply a limit on the complexity of the types we can have
Yep, but if you add a new builtin with 10 type variables and get a type error because of that, you can always extend the list of names. I just thought it would be unlikely we'd need a builtin with more than 9 type variables.
| One non-solution would be to instantiate @a@, then recurse on the type, construct a new function | ||
| that defers to the original @nullList@ but wraps its argument in a specific way (more on that below) | ||
| making it possible to assign a 'TypeScheme' to the resulting function. Astonishingly enough, that | ||
| could actually work and if we ever write a paper on builtins, we should mention that example, but: |
I believe the machinery in question is just the machinery that works out how to turn the types of builtin implementation into |
Yes, that's correct, sorry about the ambiguity. By "expressiveness" I meant the expressiveness of the
I'm gonna be documenting something along these lines next.
Yeah, I meant that we can express GADTs in Plutus Core (it's easy to do that, but compiling from actual Haskell GADTs may or may not be a nearly unsolvable problem), I've never pondered if we could express GADTs via the builtins machinery, maybe we could, dunno.
In theory we could allow a flavor of In any case currently you can't apply a function to an argument within the builtins machinery. I'm gonna play with that in future though, but I'll preserve the invariant that we only need first-order costing. |
effectfully
deleted the
effectfully/disentangle-KnownTypeAst-from-KnownTypeIn
branch
…O#4312) * [Builtins] Disentangle 'KnownTypeAst' from 'KnownTypeIn' * See Note [Unlifting values of built-in types] This generalized the `TypeScheme` inference machinery and makes it more powerful and at the same time easier to use.
Do not look here yet.