[Haskell-cafe] Size-indexed monoids

[Adam Gundry]

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/