[Haskell-cafe] Size-indexed monoids
Li-yao Xia
lysxia at gmail.com
Wed Feb 22 23:58:21 UTC 2017
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
More information about the Haskell-Cafe
mailing list