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

[Serguey Zefirov]

2012/5/17 Iavor Diatchki <iavor.diatchki at gmail.com>:
> 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 <sergueyz at 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>