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

17 May 2012

      2012/5/17 Iavor Diatchki :
...
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.
Oh, it was of great matter to me. Because constraints like that get
through type family expressions and make it hard to conceal state that
should satisfy constraints on type family expressions over the type of
the state.

I can write something like that:

data Combinator s a where
    Combinator :: Class (TypeFamExpr s) => ... -> Combinator s a

And I cannot write something like that:
data Combinator a where
    Combinator :: Class (TypeFamExpr s) => .mentions s.. -> Combinator a

If my TypeFamExpr does have type variables, I get a wild type error
messages that mentions partially computed TypeFamExpr as an argument
to constraint.

I can make more detailed example, if you wish.
...
-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  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