Support mkNil for any builtin types
#7438
Conversation
SeungheonOh
changed the title
mkNil for Bool and BuiltinByteStringmkNil for any builtin types
|
I made it so that now |
| | (tyCon, tyArg1, tyArg2) == (builtinPairTyCon, builtinDataTyCon, builtinDataTyCon) -> | ||
| pure $ PLC.mkConstant annMayInline ([] @(PLC.Data, PLC.Data)) | ||
| _ -> throwPlain $ CompilationError "'mkNil' applied to an unknown type" | ||
| | GHC.getName n == mkNilOpaqueName -> compileMkNil ty |
There was a problem hiding this comment.
even though we now match mkNil directly and have "OPAQUE" for mkNil, we still need mkNilOpaque because for some reason ghc would ignore OPAQUE and use mkNilOpaque anyways.
There was a problem hiding this comment.
I don't think we have OPAQUE for mkNil?
IIRC the point of this design was to make sure that some type class indirection doesn't get in the way, but I don't remember if it was necessary.
| -> m (PIRTerm uni fun) | ||
| compileMkNil ty = | ||
| let | ||
| tyToUniverse :: GHC.Type -> Maybe (SomeTypeIn' PLC.DefaultUni) |
There was a problem hiding this comment.
is there a way to do this with existing SomeTypeIn? SomeTypeIn won't work because it has existential kind and it's impossible to force that to Type...
There was a problem hiding this comment.
I think you can avoid existentials altogether and do something like
withCompiledMkNil :: GHC.Type -> (forall a. PLC.DefaultUni (Esc a) -> m (PIRTerm uni fun)) -> m (PIRTerm uni fun)but I also think that your version is simpler, so who cares.
effectfully
left a comment
effectfully
left a comment
There was a problem hiding this comment.
You're my hero.
This was my original idea on how to make it work in the general case:
The only more or less reliable way I could think of is serializing the type at the type level into a
Symbol(to make sure it's fully done at compile time), requiring it to beKnownSymbol, then extracting the resultingStringin the compiler and parsing it back to get aDefaultUniobject. Sounds pretty crazy, but I can't think of another way of parsing a Haskell value back after embedding it into aCoreExpr.
But that's a lot of effort for something rather insignificant and your solution should be enough in most cases (I don't wanna think when it's not enough).
I'll check if I can it statically detectable that an instance is missing.
| {- | Identical to `SomeTypeIn` but without existential kind. | ||
| -} | ||
| type SomeTypeIn' :: (Kind.Type -> Kind.Type) -> Kind.Type | ||
| data SomeTypeIn' uni = forall a. SomeTypeIn' !(uni (PLC.Esc a)) |
There was a problem hiding this comment.
Could call it SomeStarIn or something. Just nitpicking obviously.
| -> m (PIRTerm uni fun) | ||
| compileMkNil ty = | ||
| let | ||
| tyToUniverse :: GHC.Type -> Maybe (SomeTypeIn' PLC.DefaultUni) |
There was a problem hiding this comment.
I think you can avoid existentials altogether and do something like
withCompiledMkNil :: GHC.Type -> (forall a. PLC.DefaultUni (Esc a) -> m (PIRTerm uni fun)) -> m (PIRTerm uni fun)but I also think that your version is simpler, so who cares.
| | (tyCon, tyArg1, tyArg2) == (builtinPairTyCon, builtinDataTyCon, builtinDataTyCon) -> | ||
| pure $ PLC.mkConstant annMayInline ([] @(PLC.Data, PLC.Data)) | ||
| _ -> throwPlain $ CompilationError "'mkNil' applied to an unknown type" | ||
| | GHC.getName n == mkNilOpaqueName -> compileMkNil ty |
There was a problem hiding this comment.
I don't think we have OPAQUE for mkNil?
IIRC the point of this design was to make sure that some type class indirection doesn't get in the way, but I don't remember if it was necessary.
| import Data.Map qualified as Map | ||
| import Data.Text qualified as T | ||
|
|
||
| {- | Identical to `SomeTypeIn` but without existential kind. |
There was a problem hiding this comment.
Elaborate why the existential kind is problematic?
You can now use
PlutusTx.Builtins.Opaque.mkNil @BoolandmkNil @BuiltinByteString.This doesn't add support for arbitrarily nested array. Only adds support for
BoolandByteString.I'm figuring out making this work with any subtype of default universe, so please don't merge yet