[Haskell-cafe] Size-indexed monoids

[Li-yao Xia]

Hello,

This approach using unsafeCoerce is implemented by the recently added
Data.Constraints.Nat module of the constraints package, which exports
reusable proofs to help GHC reason about type-level literals. It's
definitely something very experimental, and the current version on
Hackage is unfortunately bugged, but seems worth mentioning.

http://hackage.haskell.org/package/constraints-0.9/docs/Data-Constraint-Nat.html

Li-yao

On 02/22/2017 04:35 PM, Adam Gundry wrote:
> 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