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.... Li-yao On 02/22/2017 04:35 PM, Adam Gundry 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
On 22/02/17 20:39, Sergey Kosyrev wrote: 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