Last active
November 6, 2017 22:24
-
-
Save phadej/2fc066c00e33b9486e1a3e5f7767a8d7 to your computer and use it in GitHub Desktop.
Example how is possible to write polykinded type-classes in GHC-8.0. It's not that bad or messy, but I'm not sure it's practical either.
This file contains hidden or 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
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeSynonymInstances #-} | |
-- And two extensions making the tricks possible: | |
{-# LANGUAGE TypeFamilyDependencies #-} | |
{-# LANGUAGE TypeInType #-} | |
-- This is needed for (f a) instance | |
{-# LANGUAGE UndecidableInstances #-} | |
import Data.Kind | |
import Data.Proxy | |
import GHC.Types | |
-- Type family to determine type signature of 'rnfPoly'. | |
-- We use @TypeFamilyDependencies@ to drop @'Proxy' a@ parameter from 'rnfPoly', | |
-- so compiler can infer more types for us! | |
-- | |
-- Unfortunately for higher kinds we need a newtype wrapper, as polymorphic type cannot be | |
-- a result of type-family. | |
type family NFDataSig k (a :: k) = (r :: *) | r -> a where | |
NFDataSig (*) f = f -> () | |
-- Argument can be polykinded! | |
-- We cannot have: even ImpredicativeTypes don't help here | |
-- NFDataSig (k -> l) f = forall (a :: k). NFDataSig k a -> NFDataSig l (f a) | |
NFDataSig (k -> l) f = X k l f | |
-- For not star we require only proxy, can have DataKinds as kinds! | |
NFDataSig k f = Proxy f | |
newtype X k l (f :: k -> l) = X { runX :: forall (a :: k). NFDataSig k a -> NFDataSig l (f a) } | |
{- Without newtype: | |
- Illegal polymorphic type: forall a. (a -> ()) -> f a -> () | |
-} | |
class NFData (a :: k) where | |
rnfPoly :: NFDataSig k a | |
------------------------------------------------------------------------------- | |
-- * | |
------------------------------------------------------------------------------- | |
rnf :: forall a. NFData a => a -> () | |
rnf = rnfPoly | |
instance NFData () where | |
rnfPoly () = () | |
------------------------------------------------------------------------------- | |
-- * -> * | |
------------------------------------------------------------------------------- | |
{- | |
λ *Main > let x = Just undefined :: Maybe () | |
λ *Main > :p x | |
x = Just (_t2::()) | |
λ *Main > x `seq` () | |
() | |
λ *Main > :p x | |
x = Just (_t3::()) | |
λ *Main > rnf1 x | |
*** Exception: Prelude.undefined | |
CallStack (from HasCallStack): | |
error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err | |
undefined, called at <interactive>:68:14 in interactive:Ghci4 | |
-} | |
instance NFData Maybe where | |
rnfPoly = X impl | |
where | |
impl _ Nothing = () | |
impl e (Just a) = e a | |
liftRnf :: (NFData f) => (a -> ()) -> f a -> () | |
liftRnf = runX rnfPoly | |
rnf1 :: (NFData a, NFData f) => f a -> () | |
rnf1 = runX rnfPoly rnfPoly | |
------------------------------------------------------------------------------- | |
-- Very Generic (f a) instance | |
------------------------------------------------------------------------------- | |
{- | |
λ *Main > let x = Just undefined :: Maybe () | |
λ *Main > :p x | |
x = Just (_t1::()) | |
λ *Main > x `seq` () | |
() | |
λ *Main > :p x | |
x = Just (_t2::()) | |
λ *Main > rnf x | |
*** Exception: Prelude.undefined | |
CallStack (from HasCallStack): | |
error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err | |
undefined, called at <interactive>:124:14 in interactive:Ghci1 | |
-} | |
-- Generic instance! I'm not sure if it's good idea to have it, as for some | |
-- types the context is to restrictive. | |
instance (NFData f, NFData a) => NFData (f a) where | |
rnfPoly = runX rnfPoly rnfPoly | |
------------------------------------------------------------------------------- | |
-- * -> * -> * | |
------------------------------------------------------------------------------- | |
instance NFData Either where | |
rnfPoly = X $ \l -> X $ \r -> impl l r | |
where | |
impl l _ (Left x) = l x | |
impl _ r (Right x) = r x | |
liftRnf2 :: NFData f => (a -> ()) -> (b -> ()) -> f a b -> () | |
liftRnf2 l r = runX (runX rnfPoly l) r | |
rnf2 :: (NFData a, NFData b, NFData f) => f a b -> () | |
rnf2 = runX (runX rnfPoly rnfPoly) rnfPoly | |
------------------------------------------------------------------------------- | |
-- Symbol -> * and k -> * | |
------------------------------------------------------------------------------- | |
{- | |
Unfortunately we cannot write instance for Proxy, or other polykinded types, | |
as our family could match for both (*) and some other kind | |
I suppose that we cannot do that, as we cannot write instances for universally | |
quantified types, i.e `instance Num (forall a. a -> a) where .. | |
-} | |
data SymbolP (k :: Symbol) = SymbolP | |
instance NFData SymbolP where | |
rnfPoly = X impl | |
where | |
-- impl :: NFDataSig Symbol a -> NFDataSig (*) (SymbolP a) | |
-- impl :: Proxy (SymbolP a) -> SymbolP a -> () | |
impl _ SymbolP = () | |
{- | |
We can write instances for polykinded types too. The trick is even that | |
type-family cannot reduce in this definition, but as type variable is phantom | |
we don't need that parameter at all. So it just works! | |
Note: single polykinded var: the value is most likely phantom, as you can | |
instantiate it with whatever you want. Kind-level parametricity!) | |
-} | |
instance NFData Proxy where | |
rnfPoly = X impl | |
where | |
impl _ Proxy = () | |
------------------------------------------------------------------------------- | |
-- (* -> *) -> * | |
------------------------------------------------------------------------------- | |
{- | |
λ *Main > let x = Fix (Just (Fix (Just (Fix undefined)))) :: Fix Maybe | |
λ *Main > :p x | |
x = Fix (Just (Fix (Just (_t1::a)))) | |
λ *Main > x `seq` () | |
() | |
λ *Main > :p x | |
x = Fix (Just (Fix (Just (_t2::a1)))) | |
λ *Main > rnfFix (runX rnfPoly) x | |
*** Exception: Prelude.undefined | |
CallStack (from HasCallStack): | |
error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err | |
undefined, called at <interactive>:86:35 in interactive:Ghci1 | |
-} | |
newtype Fix f = Fix (f (Fix f)) | |
instance NFData Fix where | |
rnfPoly = X impl | |
where | |
-- Vicious self-recursion! | |
impl :: NFDataSig (* -> *) f -> NFDataSig * (Fix f) | |
impl x@(X rnf') (Fix f) = rnf' (impl x) f | |
rnfFix :: forall m f. NFData m => (forall a. (a -> ()) -> f a -> ()) -> m f -> () | |
rnfFix f = runX rnfPoly (X f) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment