10

Messing around with GHC's DataKinds, I tried implementing type-level binary nats. They're simple enough to implement, but if I want them to be useful in common cases, then GHC needs to believe that the Succ type family is injective (so that type inference will work at least as well as it does for unary type-level nats). However, I'm having a difficult time convincing GHC that this is the case. Consider the following encoding of binary nats:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Nat2 where

data Nat = Zero | Pos Nat1
data Nat1 = One | Bit0 Nat1 | Bit1 Nat1
  -- by separating Nat and Nat1 we avoid dealing w/ Bit0^n Zero as a spurrious representation of 0

type family Succ (n :: Nat) :: r | r -> n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos (Succ1 x)

type family Succ1 (n :: Nat1) :: r | r -> n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('Bit0 x) = 'Bit1 x
  Succ1 ('Bit1 x) = 'Bit0 (Succ1 x)

GHC can't accept this, because it can't tell that Succ1 is injective:

Nat2.hs:12:3: error:
    • Type family equations violate injectivity annotation:
        Succ 'Zero = 'Pos 'One -- Defined at Nat2.hs:12:3
        Succ ('Pos x) = 'Pos (Succ1 x) -- Defined at Nat2.hs:13:3
    • In the equations for closed type family ‘Succ’
      In the type family declaration for ‘Succ’
   |
12 |   Succ 'Zero = 'Pos 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^

Nat2.hs:16:3: error:
    • Type family equations violate injectivity annotation:
        Succ1 'One = 'Bit0 'One -- Defined at Nat2.hs:16:3
        Succ1 ('Bit1 x) = 'Bit0 (Succ1 x) -- Defined at Nat2.hs:18:3
    • In the equations for closed type family ‘Succ1’
      In the type family declaration for ‘Succ1’
   |
16 |   Succ1 'One = 'Bit0 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^^

We think it's injective because, by inspection of Succ1, One is never in its image, so the Bit0 (Succ1 x) case never returns Bit0 One, and thus the Bit1 case will never conflict with the One case. The same argument ("One is not in the image of Succ1") shows that Succ itself is also injective. However, GHC is not quite clever enough to find this argument.

So, question: in this case (and cases like these), is there any way to convince GHC that an injective type family is in fact injective? (Perhaps a typechecker plugin where I can provide a function that inverts Succ1? Perhaps a pragma that says "try inferring backwards from this family as if it were injective; if you hit any ambiguities you're allowed to crash"?)

So8res
  • 9,856
  • 9
  • 56
  • 86
  • 1
    Doesn't your ghc complain also about Succ being non-injective? Mine does (8.2.2) – n. m. could be an AI Jan 14 '18 at 17:56
  • Yep, good catch. Edited the OP. Note that the proof that `Succ` is injective uses the same key argument as the proof that `Succ1` is injective (namely, "`One` is not in the image of `Succ1`"), so I'm hoping that any method that can convince GHC that `Succ1` is injective also works to convince it about `Succ`. – So8res Jan 14 '18 at 18:30
  • I'm curious: what happens if you switch to a more regular zeroless representation, like `data Bit = One | Two; type Nat = [Bit]`, or perhaps `data Nat = Zero | Bit1 Nat | Bit2 Nat`? If you can't make those work, your chances of making something fancier work seem pretty slim. – dfeuer Jan 14 '18 at 18:45
  • 1
    The trouble with `data Nat = Zero | Bit1 Nat | Bit2 Nat` is that in that case, the function `Succ` *isn't* injective: `Succ Zero` and `Succ (Bit0 Zero)` both map to `Bit1 Zero`. The hope is that, given a representation of binary nats where `Succ` *is* injective, GHC can be made to believe this (or at least take it on my word). – So8res Jan 14 '18 at 19:21
  • 1
    @So8res, there is no `Bit0` in the representation I mentioned--it's 1-2 rather than 0-1. – dfeuer Jan 14 '18 at 19:28
  • Well, what I was attempting doesn't seem to work anyway. Oh well. – dfeuer Jan 14 '18 at 22:14
  • @dfeuer oh, neat. But yeah, that still requires convincing GHC somehow to accept an argument of the form "I should be allowed to recurse here because the only potentially ambiguous output does not appear in the image of the function" – So8res Jan 15 '18 at 00:12
  • I've messed around a bit with an encoding of numbers as a non-empty sequence of streaks of 0- and 1-bits, where each streak length is encoded as a Peano-style positive number. You need an indication of the number being even or odd. There's an implicit MSB of 1 after the sequence. 0 is encoded separately as in your scheme. It is very difficult to work with this encoding so I didn't finish it, but it looks like increment could be injective in it (it involves at most 3 streaks so all cases may be listed explicitly). – n. m. could be an AI Jan 15 '18 at 06:52

0 Answers0