Uh oh!
There was an error while loading. Please reload this page.
Add function to convert from explicit Type values to implicit Typed constraints
#752
RyanGlScott
started this conversation in
General
Replies: 0 comments
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
While studying the code in
copilot-corerecently, I noticed that there are many places that redundantly storeTypes at runtime. For instance, consider the definition ofcopilot-core'sArray:copilot/copilot-core/src/Copilot/Core/Type.hs
Lines 154 to 156 in 4e5fd9a
This has both a
Typed tconstraint as well as aType tvalue. We see something similar in theSpecdata constructor, which has both aTyped aconstraint and aType afield:copilot/copilot-core/src/Copilot/Core/Spec.hs
Lines 40 to 45 in 4e5fd9a
There's nothing incorrect about doing this, but it is wasteful. At runtime,
Typeddictionaries already store aTypevalue (by way of thetypeOfmethod), so one could get rid of theTypefields in favor of just theTypedconstraints. Doing so would save some space every time GHC allocates aTypeat runtime.Alternatively, we could get rid of the
Typedconstraints in favor of just storing aTypefield. In order to do this, however, we would need to be able to convert fromType(an explicit, value-level representation) toTyped(an implicit constraint). Currently, thecopilot-coreAPI does not offer a way to do this. I propose we add one. I'm thinking of a function with this type signature:This would be analogous to the Haskell standard library's
withTypeablefunction. A simplistic way to implementwithTypedwould be:Alternatively, we could make
withTypeda no-op at runtime if we are willing to use GHC'swithDictprimitive. (Doing so would require changingTypedto a single-method type class, so that is probably worth a separate discussion.)All reactions