Haskell/GHC: How to write predicates on type-level naturals

Question

I could have sworn I saw an article on this recently, but I can't find it.

I'm trying to make a type to do binary encoding of the numbers mod n, but to do so, I need to be able to write predicates on the type level naturals:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Modulo where

-- (pseudo-)binary representation of 
-- numbers mod n
--
--  e.g. Mod Seven contains
--    Zero . Zero . Zero $ Stop
--    Zero . Zero . One  $ Stop
--    Zero . One . Zero $ Stop
--    Zero . One . One  $ Stop
--    One . Zero . Zero $ Stop
--    One . Zero . One  $ Stop
--    One . One $ Stop 
data Mod n where
  Stop :: Mod One
  Zero :: Split n => Mod (Lo n) -> Mod n
  One  :: Split n => Mod (Hi n) -> Mod n

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- predicate to allow us to compare 
-- natural numbers
class Compare n n' b | n n' -> b

-- type-level ordering
data LT
data EQ
data GT

-- base cases
instance Compare One One EQ
instance Compare One (Succ n) LT
instance Compare (Succ n) One GT

-- recurse
instance Compare n n' b => Compare (Succ n) (Succ n') b

-- predicate to allow us to break down
-- natural numbers by their bit structure
--
-- if every number mod n can be represented in m bits, then
class Split n where
  type Lo n -- number of values mod n where the m'th bit is 0
  type Hi n -- number of values mod n where the m'th bit is 1

-- base case, n = 2
-- for this, we only need m=1 bit
instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

-- recurse
--  if (Lo n) == (Hi n), then n = 2^m, so
--  the values mod (n+1) will require one extra bit
instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n) where
  type Lo (Succ n) = n    -- all the numbers mod n will be prefixed by a 0
  type Hi (Succ n) = One  -- and one extra, which will be 10...0

-- recurse
--  if (Lo n) > (Hi n), then n < 2^m, so
--  the values mod (n+1) still only require m bits
instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n) where
  type Lo (Succ n) = Lo (n)       -- we've got the same number of lower values
  type Hi (Succ n) = Succ (Hi n)  -- and one more higher value

My current implementation spits out a bunch of compiler errors:

Nat.hs:60:8:
    Conflicting family instance declarations:
      type Lo Two -- Defined at Nat.hs:60:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:61:8:
    Conflicting family instance declarations:
      type Hi Two -- Defined at Nat.hs:61:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Nat.hs:66:10:
    Duplicate instance declarations:
      instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n)
        -- Defined at Nat.hs:66:10-62
      instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n)
        -- Defined at Nat.hs:73:10-62

Nat.hs:67:8:
    Conflicting family instance declarations:
      type Lo (Succ n) -- Defined at Nat.hs:67:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:68:8:
    Conflicting family instance declarations:
      type Hi (Succ n) -- Defined at Nat.hs:68:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Which makes me think I'm going about writing my predicates wrong, if it thinks they're conflicting.

How can I do them right?

Buerger

By "naturals", do you mean "natural numbers"? – Elma

Type families and overlapping instances don't work together right now. Take a peek over at hackage.haskell.org/trac/ghc/ticket/4259 – Luigi

Answer 1

The conflict problem is simple enough. The rules for overlapping type families are quite simple:

The instance declarations of a type family used in a single program may only overlap if the right-hand sides of the overlapping instances coincide for the overlapping types. More formally, two instance declarations overlap if there is a substitution that makes the left-hand sides of the instances syntactically the same. Whenever that is the case, the right-hand sides of the instances must also be syntactically equal under the same substitution.

Note that it specifies syntactically equal. Consider these two instances:

instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

instance Split (Succ n) where
  type Lo (Succ n) = Lo (n)  
  type Hi (Succ n) = Succ (Hi n)

Two is defined as Succ One, and plain type synonyms are expanded for purposes of syntactic equality, so these are equal on the left-hand sides; but the right-hand sides are not, hence the error.

You may have noticed that I removed the class context from the above code. The deeper problem, and perhaps why you didn't expect the above conflict to occur, is that the duplicate instances really are conflicting duplicates. Class contexts are, as always, ignored for purposes of instance selection, and if memory serves me this goes double for associated type families, which are largely a syntactic convenience for unassociated type families and may not be constrained by the class in ways you'd expect.

Now, clearly those two instances should be distinct, and you'd like to chose between them based on the result of using Compare, therefore that result must be a parameter of the type class, not merely a constraint. You're also mixing type families with functional dependencies here, which is needlessly awkward. So, starting from the top, we'll keep the basic types:

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- type-level ordering
data LT
data EQ
data GT

Rewrite the Compare function as a type family:

type family Compare n m :: *
type instance Compare One One = EQ
type instance Compare (Succ n) One = GT
type instance Compare One (Succ n) = LT
type instance Compare (Succ n) (Succ m) = Compare n m

Now, to handle the conditional we'll need some sort of "flow control" type family. I'll define something a bit more general here for edification and inspiration; specialize according to taste.

We'll give it a predicate, an input, and two branches to chose from:

type family Check pred a yes no :: * 

We'll need a predicate for testing Compare's result:

data CompareAs a
type instance (CompareAs LT) LT yes no = yes 
type instance (CompareAs EQ) LT yes no = no
type instance (CompareAs GT) LT yes no = no
type instance (CompareAs LT) EQ yes no = no 
type instance (CompareAs EQ) EQ yes no = yes
type instance (CompareAs GT) EQ yes no = no
type instance (CompareAs LT) GT yes no = no
type instance (CompareAs EQ) GT yes no = no
type instance (CompareAs GT) GT yes no = yes

That's a frightfully tedious set of definitions, granted, and the prognosis is quite grim for comparing larger sets of type-values. More extensible approaches exist (a pseudo-kind tag and a bijection with the naturals being an obvious and effective solution) but that's a bit beyond the scope of this answer. I mean, we're just doing type-level computation here, let's not get ridiculous or anything.

Simpler in this case would be to simply define a case analysis function on comparison results:

type family CaseCompare cmp lt eq gt :: *
type instance CaseCompare LT lt eq gt = lt
type instance CaseCompare EQ lt eq gt = eq
type instance CaseCompare GT lt eq gt = gt

I'll use the latter for now, but if you want more complex conditionals elsewhere a generic approach begins to make more sense.

Anyway. We can split the... er, Split class into unassociated type families:

data Oops

type family Lo n :: *
type instance Lo Two = One
type instance Lo (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  (Succ n)
                  (Lo (Succ n))

type family Hi n :: *
type instance Hi Two = One
type instance Hi (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  One
                  (Succ (Hi (Succ n)))

The most significant point here is the (seemingly redundant) use of (Succ (Succ n))--the reason for this is that two Succ constructors are necessary to distinguish the argument from Two, thus avoiding the conflict errors you saw.

Note that I've moved everything to type families here for simplicity, as it's all entirely type-level. If you also wish to handle values differently depending on the above calculations--including indirectly, via the Mod type--you may need to add appropriate class definitions back, since those are required for choosing terms based on type, rather than merely choosing types based on types.

Ostracod