Kind classes and associated closed type families
Ryan Scott
ryan.gl.scott at gmail.com
Fri Dec 18 18:37:13 UTC 2015
Thanks to Richard's hard work, I can now define kind classes!
class Extractable k where
type Extract (n :: Nat) (x :: k) :: y
(For context, Extract is something roughly resembling the X type
family in the paper Generic Programming for Indexed Datatypes. [1])
This is really, really cool. Except that when I tried using this
class, I quickly ran into issues:
instance Extractable (a, b) where
type Extract 0 '(l, _) = l
type Extract 1 '(_, r) = r
type Extract _ _ = TypeError ('Text "out of bounds")
This yields the error:
Extractable.hs:16:8: error:
Conflicting family instance declarations:
forall a b (r :: b) (_ :: a).
Extract 1 '(_, r) = r -- Defined at Extractable.hs:16:8
forall a b (_ :: Nat) (_1 :: (a, b)) y.
Extract _ _1 = (TypeError ...) -- Defined at Extractable.hs:17:8
It hit me as to why: GHC is interpreting each Extract type instance as
being separate from each other, not as a part of a single, closed type
family over kind (a, b). And as it turns out, GHC does not allow
closed associated type families. [2]
That leads me to wonder: is there a particular reason why GHC couldn't
allow closed associated type families? Because of this restriction, I
have to define the Extractable (a, b) instance like this:
instance Extractable (a, b) where
type Extract n p = ExtractPair n p
type family ExtractPair (n :: Nat) (x :: (a, b)) :: y where
ExtractPair 0 '(a, _) = a
ExtractPair 1 '(_, b) = b
ExtractPair _ _ = TypeError ('Text "out of bounds")
But that requires -XUndecidableInstances, and makes it much more
difficult to examine type family reductions with GHCi's :kind!
command.
Ryan S.
-----
[1] http://dreixel.net/research/pdf/gpid.pdf
[2] https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#synonym-families
More information about the ghc-devs
mailing list