Created
June 16, 2020 13:02
-
-
Save tscholak/c5766447f3ab0ab2fbde88d4612ff154 to your computer and use it in GitHub Desktop.
little exercise in constrained existential types
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data E (c :: k -> Constraint) (f :: k -> Type) = forall a . c a => E { unE :: f a } | |
runE :: forall b c f . (forall a . c a => f a -> b) -> E c f -> b | |
runE g (E a) = g a | |
-- this says that when I have a value of type 'E c f' where 'c' is a type-level function from kinds to constraints | |
-- and 'f' is a data type with one kind parameter, then I can apply any function | |
-- | |
-- @ | |
-- g :: forall a . c a => f a -> b | |
-- @ | |
-- | |
-- on that value. | |
-- the type 'a' is not statically known and can be anything that fulfills the constraint | |
newtype UnknownDeviceTensor device = UnknownDeviceTensor { unWrap :: Tensor device 'D.Float '[] } | |
test :: E KnownDevice UnknownDeviceTensor -> D.Device | |
test = runE (device . unWrap) | |
-- of course, in the example 'test' I’m cheating a bit. | |
-- Because, in order to get a value of E KnownDevice UnknownDeviceTensor, I need to know the device: | |
mkE :: E KnownDevice UnknownDeviceTensor | |
mkE = E (UnknownDeviceTensor (ones @'[] @'D.Float @'( 'D.CPU, 0))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment