[Haskell-cafe] Data Kinds and superfluous (in my opinion) constraints contexts

[Simon Peyton-Jones]

I'm glad you've been trying out kinds.  However, I don't understand the feature you want here.

You say:

fromIntgr :: Integer -> BV (size :: D) 
fromIntgr int = BV mkD int   -- doesn't work, but desired.

fromIntgr :: MkD size => Integer -> BV (size :: D) 
fromIntgr int = BV mkD int   -- does work, but is not that useful.

The implementation MUST pass a value parameter for (MkD size =>) to fromIntgr. Your point is presumably that since every inhabitant of kind D is an instance of MkD, the (MkD size =>) doesn't actually constrain the type at all. It really works for every instantiation of 'size'.

So maybe your feature is

  Please omit class constraints where I can see that 
  every suitably-kinded argument is an instance of the
  class.

I suppose that might be conceivable, but it'd make the language more complicated, and the implementation, and I don't see why the second version is "not that useful".

Start a feature-request ticket if you like, though.

Simon

| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-
| bounces at haskell.org] On Behalf Of Serguey Zefirov
| Sent: 06 May 2012 17:49
| To: haskell
| Subject: [Haskell-cafe] Data Kinds and superfluous (in my opinion)
| constraints contexts
| 
| 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe