wip: Implement typesystem #40
Conversation
This is not super useful at the moment, as it doesn't shrink. The design is also in flux at the moment. It makes more sense to remove this for now and implement it once things are more stable.
Removed Internal.ASGType module and colocated the type definitions next to the types where it is relevant. Implemented typing for `PrimCall`s
src/Covenant/Prim.hs
Outdated
| FstPair -> (TyPair TyPlutusData TyPlutusData, TyPlutusData) | ||
| SndPair -> (TyPair TyPlutusData TyPlutusData, TyPlutusData) | ||
| HeadList -> (TyList TyPlutusData, TyPlutusData) | ||
| TailList -> (TyList TyPlutusData, TyList TyPlutusData) |
There was a problem hiding this comment.
@kozross This PR doesn't include rank-1 polymorphism. I'll add that in a future PR.
For now, I'm using TyPlutusData as a placeholder for polymorphic types.
| @@ -185,12 +199,16 @@ bound Scope = Bound . fromIntegral . natVal $ Proxy @n | |||
| -- @since 1.0.0 | |||
| lam :: | |||
| forall (n :: Natural) (m :: Natural). | |||
| ASGType -> | |||
There was a problem hiding this comment.
We need to update the documentation to specify that this is the intended type of the argument, not the type of the lambda as a whole.
| @@ -209,16 +227,34 @@ lam Scope f = do | |||
| -- @since 1.0.0 | |||
| letBind :: | |||
| forall (n :: Natural) (m :: Natural). | |||
| ASGType -> | |||
src/Covenant/Internal/ASGBuilder.hs
Outdated
| -- | The errors that come up while resolving types. | ||
| -- | ||
| -- @since 1.0.0 | ||
| data TypeError | ||
| = TyErrAppNotALambda ASGType | ||
| | TyErrAppArgMismatch ASGType ASGType -- expected, received | ||
| | TyErrPrimNotAConstant ASGType | ||
| | TyErrPrimArgMismatch (Vector TyConstant) (Vector TyConstant) -- exptected, received | ||
| | TyErrNonHomogenousList |
There was a problem hiding this comment.
These constructors should have Haddocks of their own explaining their meaning. While in some cases it's fairly clear (TyErrAppNotALambda for example), in others, it's not TyErrAppArgMismatch would require me to read the source code to understand which field was which).
src/Covenant/Constant.hs
Outdated
| -- | The type of Plutus constant terms. | ||
| -- | ||
| -- @since 1.0.0 | ||
| data TyConstant |
There was a problem hiding this comment.
This is slightly misnamed: ByteStrings for example aren't necessarily constants, as we can construct them from other operations (such as ConsByteString). From what I can see later-on, this seems to be a general 'type of Covenant expression', which means it's missing a couple of things (such as BLS types for example).
src/Covenant/Prim.hs
Outdated
| BLS12_381_G1_neg -> (TyByteString, TyByteString) | ||
| BLS12_381_G1_compress -> (TyByteString, TyByteString) | ||
| BLS12_381_G1_uncompress -> (TyByteString, TyByteString) | ||
| BLS12_381_G2_neg -> (TyByteString, TyByteString) | ||
| BLS12_381_G2_compress -> (TyByteString, TyByteString) | ||
| BLS12_381_G2_uncompress -> (TyByteString, TyByteString) |
There was a problem hiding this comment.
Many of these do not consume, or produce, ByteStrings - they produce and consume the corresponding BLS types. The only ones that take or return ByteStrings are compression and uncompression primitives.
src/Covenant/Prim.hs
Outdated
| BLS12_381_G1_add -> (TyByteString, TyByteString, TyByteString) | ||
| BLS12_381_G1_scalarMul -> (TyInteger, TyByteString, TyByteString) | ||
| BLS12_381_G1_equal -> (TyByteString, TyByteString, TyBoolean) | ||
| BLS12_381_G1_hashToGroup -> (TyByteString, TyByteString, TyByteString) | ||
| BLS12_381_G2_add -> (TyByteString, TyByteString, TyByteString) | ||
| BLS12_381_G2_scalarMul -> (TyInteger, TyByteString, TyByteString) | ||
| BLS12_381_G2_equal -> (TyByteString, TyByteString, TyBoolean) | ||
| BLS12_381_G2_hashToGroup -> (TyByteString, TyByteString, TyByteString) | ||
| BLS12_381_millerLoop -> (TyByteString, TyByteString, TyByteString) | ||
| BLS12_381_mulMlResult -> (TyByteString, TyByteString, TyByteString) | ||
| BLS12_381_finalVerify -> (TyByteString, TyByteString, TyBoolean) |
src/Covenant/Prim.hs
Outdated
| CaseData -> | ||
| ( TyPlutusData, | ||
| TyPair TyInteger (TyList TyPlutusData), | ||
| TyList (TyPair TyPlutusData TyPlutusData), | ||
| TyList TyPlutusData, | ||
| TyInteger, | ||
| TyByteString, | ||
| TyPlutusData | ||
| ) |
There was a problem hiding this comment.
If you look at the stated semantics of CaseData, you will see that it doesn't take arbitrary polymorphic terms, but instead functions with a polymorphic return type. I assume that this is just 'shorthanded' the same way as other polymorphic functions?
There was a problem hiding this comment.
Thanks for catching this. I meant to update this once I figure out the function types in AConstant.
For some reason I thought PrimCall can only accept constants.
These were not shorthanded, I'll replace these with TyLam.
There was a problem hiding this comment.
CaseData is a somewhat unusual situation, as it's the only builtin that does this.
| runASGBuilder :: ASGBuilder a -> ASGBuilderState -> (Either ASGBuilderError a, ASGBuilderState) | ||
| runASGBuilder (ASGBuilder m) s = | ||
| let stateM = runExceptT m | ||
| in runState stateM s |
There was a problem hiding this comment.
This is a bit different to the original, and unfortunately isn't doing quite what we want. The reason why the original builder runner worked the way it did was because, by forcing the monad to produce a result of type Id, we ensure we have a toplevel computation, which this does not do.
There was a problem hiding this comment.
Do you mean we should restrict the type of runASGBuilder to accept ASGBuilder Id or we should flip the order of State and Either in the stack?
If it's the latter case, it would just make the partial state unavailable in the case of an error, right? It wouldn't ensure we have a top-level computation?
|
Closing in favor of #45 |
No description provided.