Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Store constants in a data instance #4200

Conversation

effectfully
Copy link
Contributor

This is another attempt at Kmett's idea to store constants in a data instance (the previous one was #4196). Largely straightforward, there's just one slight twist.

Don't look here yet. There are no docs and this PR needs to be benchmarked first.

Copy link
Contributor

@michaelpj michaelpj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know you said not to look but I did anyway sorry. Not too bad at all, in the end!

@@ -337,6 +342,17 @@ data Kinded uni ta where
type ValueOf :: (Type -> Type) -> Type -> Type
data ValueOf uni a = ValueOf !(uni (Esc a)) !a

type HiddenValueOf :: (Type -> Type) -> Type
data family HiddenValueOf uni
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why not make this a member of the HasHiddenValueOf class?

@@ -337,6 +342,17 @@ data Kinded uni ta where
type ValueOf :: (Type -> Type) -> Type -> Type
data ValueOf uni a = ValueOf !(uni (Esc a)) !a

type HiddenValueOf :: (Type -> Type) -> Type
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

name bikeshedding: SpecializedValueOf? Since basically the point is to be a specialized version of ValueOf for the given universe.

@@ -417,6 +433,10 @@ someValueOf uni = Some . ValueOf uni
someValue :: forall a uni. uni `Includes` a => a -> Some (ValueOf uni)
someValue = someValueOf knownUni

-- | Wrap a value into @HiddenValueOf uni@, provided its type is in the universe.
hiddenValue :: forall a uni. (HasHiddenValueOf uni, uni `Includes` a) => a -> HiddenValueOf uni
hiddenValue = hiddenValueOf knownUni
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if fromSomeValueOf . someValueOf knownUni would optimize as well.

@michaelpj
Copy link
Contributor

/benchmark

@michaelpj michaelpj mentioned this pull request Nov 26, 2021
9 tasks
@michaelpj
Copy link
Contributor

It appears to be worse! #4243 (comment)

However, I wonder if we'd only really benefit from this if we specialized the CEK machine on uni. I tried that before on another branch somewhere... maybe it would change things.

@effectfully
Copy link
Contributor Author

effectfully commented Nov 28, 2021

Superseded by #4249.

@effectfully effectfully deleted the effectfully/builtins/introduce-HiddenValueOf branch November 28, 2021 14:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants