[Haskell-cafe] Size-indexed monoids
Adam Gundry
adam at well-typed.com
Wed Feb 22 21:35:28 UTC 2017
On 22/02/17 20:39, Sergey Kosyrev wrote:
> The suspicion is that it is due to the fact that, while seductive to use (esp. due to TypeOperators),
> TypeLits.Nat carries no inductive proof of structure, which, on the other hand you have provided
> with the bespoke TMonoid-associated type families.
>
> Does anybody know if this can be overcome with the current state of art of GHC type-level machinery,
> or that we are, indeed, condemned to use the (somewhat) ugly-ish explicitly-inductive numerals?
I don't believe this is possible without cheating (see below) or using a
plugin. That said, some of the ugliness of inductive numerals can be
avoided by defining a type family to translate TypeLits.Nat into
inductive form.
> I remember people seeking to employ GHC plugins to make it more conducive to type-level
> arithmetics, but I don't really feel confident to derive judgements about their relevance and
> implications on the case..
You might take a look at the rather lovely ghc-typelits-natnormalise
plugin. I haven't tried, but assuming you adjust the code to use a type
equality constraint rather than CmpNat, I think it should automatically
solve the problematic constraint.
If you'd prefer blatant cheating, another approach is to use
unsafeCoerce, like this:
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, TypeInType,
TypeOperators, UnicodeSyntax, StandaloneDeriving,
TypeApplications, RankNTypes, ScopedTypeVariables,
AllowAmbiguousTypes, ConstraintKinds #-}
module SizeIndexedMonoids where
import GHC.TypeLits
import GHC.Types (Type)
import Unsafe.Coerce
-- | Assert without proof that the constraint c holds. It had better
-- be a true type equality constraint, otherwise you are asking for
-- trouble.
unsafeLemma :: forall c r . (c => r) -> r
unsafeLemma = unQ . (unsafeCoerce :: Q c r -> Q (r ~ r) r) . MkQ
newtype Q c r = MkQ { unQ :: c => r }
type Associativity x y z = (x + (y + z)) ~ ((x + y) + z)
data T (p :: Type) (size ∷ Nat) where
TZ ∷ T p 0
TS ∷ (Show p, (1 + m) ~ n) ⇒
{ payload ∷ p
, next ∷ T a m } → T a n
deriving instance Show p ⇒ Show (T p s)
mmappend :: forall p m n . T p m -> T p n -> T p (m + n)
mmappend TZ tr = tr
mmappend (TS pl (nl :: T a m1)) tr =
unsafeLemma @(Associativity 1 m1 n) (TS pl (mmappend nl tr))
Sorry,
Adam
> Here is the record of my failure:
>
>> {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, TypeInType, TypeOperators, UnicodeSyntax, StandaloneDeriving #-}
>>
>> module Understanding.Types where
>>
>> import GHC.TypeLits
>> import GHC.Types (Type)
>>
>> data T p (size ∷ Nat) where
>> TZ ∷ T p 0
>> TS ∷ (Show p, CmpNat (m + 1) n ~ EQ) ⇒
>> { payload ∷ p
>> , next ∷ T a m } → T a n
>> deriving instance Show p ⇒ Show (T p s)
>>
>> class MeasuredMonoid a where
>> mmempty ∷ a 0
>> mmappend ∷ a n → a m → a (n + m)
>>
>> instance MeasuredMonoid (T p) where
>> mmempty = TZ
>> mmappend TZ TZ = TZ
>> mmappend TZ t@(TS _ _) = t
>> mmappend t@(TS _ _) TZ = t
>> mmappend tl@(TS pl nl) tr = TS pl $ mmappend nl tr
>
> -- * Failure due to lack of inductive structure of GHC.TypeLits.Nat
> --
> -- error:
> -- • Could not deduce: CmpNat ((m1 + m) + 1) (n + m) ~ 'EQ
> -- arising from a use of ‘TS’
> -- from the context: (Show p1, CmpNat (m1 + 1) n ~ 'EQ)
> -- bound by a pattern with constructor:
> -- TS :: forall k (a :: k) (n :: Nat) p (m :: Nat).
> -- (Show p, CmpNat (m + 1) n ~ 'EQ) =>
> -- p -> T a m -> T a n,
> -- in an equation for ‘mmappend’
> -- at /home/deepfire/src/haskell-understanding/Types.hs:24:16-23
> -- • In the expression: TS pl
> -- In the expression: TS pl $ mmappend nl tr
> -- In an equation for ‘mmappend’:
> -- mmappend tl@(TS pl nl) tr = TS pl $ mmappend nl tr
> -- • Relevant bindings include
> -- tr :: T p m
> -- (bound at /home/deepfire/src/haskell-understanding/Types.hs:24:27)
> -- nl :: T p m1
> -- (bound at /home/deepfire/src/haskell-understanding/Types.hs:24:22)
> -- tl :: T p n
> -- (bound at /home/deepfire/src/haskell-understanding/Types.hs:24:12)
> -- mmappend :: T p n -> T p m -> T p (n + m)
> -- (bound at /home/deepfire/src/haskell-understanding/Types.hs:21:3)
>
> --
> take care,
> Kosyrev Serge
--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
More information about the Haskell-Cafe
mailing list