Hello,
The context in your example serves an important purpose: it records the fact that the behavior of the function may differ depending on which type it is instantiated with. This is quite different from ordinary polymorphic functions, such as `const` for example, which work in exactly the same way, no matter how you instantiate them. Note that it doesn't matter that we can solve the constraint for all types of kind `D`---the constraint is there because we can't solve it _uniformly_ for all types.
-Iavor
PS: As an aside, these two forms of polymorphism are sometimes called "parametric" (when functions work in the same way for all types), and "ad-hoc" (when the behavior depends on which type is being used).
On Sun, May 6, 2012 at 9:48 AM, Serguey Zefirov
<sergueyz@gmail.com> wrote:
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
-----------------------------------------------------------------------------------------
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe