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

[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.

-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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120516/87b61125/attachment.htm>