Hi Simon
On 10 May 2012, at 13:19, Simon Peyton-Jones wrote:
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.
So we're dealing with the difference between pi and forall. It's
clear that "promotion" alone doesn't really deliver the pi
behaviour. That still currently requires the singleton construction,
which SHE automates, at least in simple cases.
(Shameless plug: see my answer on StackOverflow this morning
http://stackoverflow.com/questions/10529360/recursively-defined-instances-and-constraints)
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.
There's a bunch of competing notions to negotiate. Once we have
a promotable type, e.g.,
data Nat = Zero | Succ Nat
we get a singleton family
data Natty :: Nat -> * where
Zeroy :: Natty Zero
Succy :: Natty n -> Natty (Suc n)
(In fact, SHE has one data family for the singleton construction, and
generates suitable data instance declarations, here mapping Nat to
Natty.)
As Serguey makes clear, we should also get a class like
class HasNatty :: Nat -> Constraint where
natty :: Natty n
instance HasNatty Zero where
natty = Zeroy
instance HasNatty n => HasNatty (Succ n) where
natty = Succy natty
Again, SHE automates this construction. The constraint HasNatty n is
written (with distinctive ugliness) {:n :: Nat:}, as is the witness,
desugaring to the equivalent of (natty :: Natty n).
We can then play spot-the-difference between
(1) forall (n :: Nat).
(2) forall (n :: Nat). Natty n ->
(3) forall (n :: Nat). HasNatty n =>
(1) is genuinely different; (2) and (3) are equivalent but have
different
pragmatics. (1) does not involve any runtime data, and has stronger
free theorems; (2) involved runtime data passed explicitly and readily
pattern-matched (for which SHE also has a notational convenience); (3)
involves runtime data passed implicitly. (2) is somehow the explicit pi
of dependent type theory (and it's how SHE translates pi); (3) is
somehow
the "implicit pi"; (1) is somehow the "irrelevant pi" (which is an abuse
of the letter pi, as the notion is an intersection rather than a
product).
I'd like to be able to (and SHE lets me) write (2) as
pi (n :: Nat).
I'd like to be able to (and SHE doesn't let me) write (3) as
(n :: Nat) =>
I see one main dilemma and then finer variations of style. The dilemma
is
EITHER make forall act like pi for promoted datatypes, so that runtime
witnesses are always present
OR distinguish pi from forall, and be explicit when runtime
witnesses
are present
Traditional type theory does the former but is beginning to flirt with
the
latter, for reasons (better parametricity, more erasure) that have
value in
theory and practice. I regard the latter as a better fit with Haskell in
any case.
However, it would be good to automate the singleton construction and
sugar over the problem, and even better to avoid the singleton
construction
just using Nat data in place of Natty data.
Other dilemmas. If we have have distinct pi and forall, which do we get
when we leave out quantifiers? I'd suggest forall, as somehow the better
fit with silence and the more usual in Haskell, but it's moot. When we
write
instance Applicative (Vector n) -- (X)
we currently mean, morally,
instance forall (n :: Nat). Applicative (Vector n) -- (X)
which we can't define, because pure needs the length at runtime. But
perhaps we should write
instance pi (n :: Nat). Applicative (Vector n)
or (if this syntax is unambiguous)
instance (n :: Nat) => Applicative (Vector n)
both of which would bring n into scope as a runtime witness susceptible
to case analysis.
There is certainly something to be done (and SHE already does some of
it,
within the limitations of a preprocessor). I'd be happy to help kick
ideas
around, if that's useful.
All the best
Conor
Simon
| -----Original Message-----
| From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe-
| boun...@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@haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
