[Haskell-cafe] Data Kinds and superfluous (in my opinion) constraints contexts
Serguey Zefirov
sergueyz at gmail.com
Sun May 6 18:48:53 CEST 2012
I decided to take a look at DataKinds extension, which became
available in GHC 7.4.
My main concerns is that I cannot close type classes for promoted data
types. Even if I fix type class argument to a promoted type, the use
of encoding function still requires specification of context. I
consider this an omission of potentially very useful feature.
Example is below.
-----------------------------------------------------------------------------------------
{-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, TypeFamilies,
UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
-- a binary numbers.
infixl 5 :*
data D =
D0
| D1
| D :* D
deriving Show
-- encoding for them.
data EncD :: D -> * where
EncD0 :: EncD D0
EncD1 :: EncD D1
EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)
-- decode of values.
fromD :: D -> Int
fromD D0 = 0
fromD D1 = 1
fromD (d :* d0) = fromD d * 2 + fromD d0
-- decode of encoded values.
fromEncD :: EncD d -> Int
fromEncD EncD0 = 0
fromEncD EncD1 = 1
fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b
-- constructing encoded values from type.
-- I've closed possible kinds for class parameter (and GHC
successfully compiles it).
-- I fully expect an error if I will try to apply mkD to some type
that is not D.
-- (and, actually, GHC goes great lengths to prevent me from doing that)
-- By extension of argument I expect GHC to stop requiring context
with MkD a where
-- I use mkD "constant function" and it is proven that a :: D.
class MkD (a :: D) where
mkD :: EncD a
instance MkD D0 where
mkD = EncD0
instance MkD D1 where
mkD = EncD1
-- But I cannot omit context here...
instance (MkD a, MkD b) => MkD (a :* b) where
mkD = EncDStar mkD mkD
data BV (size :: D) where
BV :: EncD size -> Integer -> BV size
bvSize :: BV (size :: D) -> Int
bvSize (BV size _) = fromEncD size
-- ...and here.
-- This is bad, because this context will arise in other places, some of which
-- are autogenerated and context for them is incomprehensible to human
-- reader.
-- (they are autogenerated precisely because of that - it is tedious
and error prone
-- to satisfy type checker.)
fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
-- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does work,
but is not that useful.
fromIntgr int = BV mkD int
-----------------------------------------------------------------------------------------
More information about the Haskell-Cafe
mailing list