Adding a constraint to Clash.Sized.Vector.dfold

[IchiroKawashima]

Hi,

I wounded why Clash.Sized.Vector.dfold and Clash.Sized.Vector.dtfold don't have a constraint l <= k - 1 although the range of l is obvious (i.e. 0 .. k - 1).

The lack of the constraint is quite inconvenient. For example, I wanted to implement a priority encoder circuit with dfold like this:

data PriorityEncoder (k :: Nat) (f :: TyFun Nat Type) :: Type
type instance Apply (PriorityEncoder k) l = (BitVector l, BitVector (2 ^ (k - l)))

priorityEncoder :: forall (k :: Nat) . (KnownNat k, 1 <= k) => BitVector (2 ^ k) -> BitVector k
priorityEncoder x = fst $ dfold (Proxy @(PriorityEncoder k)) encode (def, x) $ repeat ()
  where
    encode :: forall (l :: Nat)
            . (KnownNat l, l <= k - 1)
           => SNat l
           -> ()
           -> PriorityEncoder k @@ l
           -> PriorityEncoder k @@ (l + 1)
    encode SNat () (acc, remnant) =
        case plusMonotone1 @l @(k - 1) @1 *** plusMinusInverse3 @1 @k of
            Sub Dict | bitToBool $ reduceOr lowerBits -> (acc ++# 0, lowerBits)
                     | otherwise                      -> (acc ++# 1, higherBits)
                where (higherBits, lowerBits) = split remnant

But, we cannot define the circuit with dfold now because there is a variable whose bit width decreases for each iteration step (i.e. acc) by using the decreasing number k - l. There, we need to convince the ghc compiler that k - l is a valid natural number with the constraint l <= k - 1 as described in the type signature of encode which dfold doesn't accept.

I think the constraint should be added to dfold and dtfold which is necessary for handling l in the function passed to the folding functions.

Thank you.

[christiaanb]

Mmmm... right now it seems that I can't implement it because the constraints package doesn't have an axiom that is the "inverse" of plusMonotone1:

plusMonotone1' :: forall a b c . (a + c <= b + c) :- (a <= b)

because when I try to implement:

dfold :: forall p k a . KnownNat k
      => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
      -> (forall l . (l <= k - 1) => SNat l -> a -> (p @@ l) -> (p @@ (l + 1)))
      -- ^ Function to fold.
      --
      -- __NB__: The @SNat l@ is __not__ the index (see (`!!`)) to the
      -- element /a/. @SNat l@ is the number of elements that occur to the
      -- right of /a/.
      -> (p @@ 0) -- ^ Initial element
      -> Vec k a -- ^ Vector to fold over
      -> (p @@ k)
dfold _ f z xs = go (snatProxy (asNatProxy xs)) xs
  where
    go :: forall n . (n <= k) => SNat n -> Vec n a -> (p @@ n)
    go _ Nil                        = z
    go s (y `Cons` (ys :: Vec (n - 1) a)) =
      let s' = s `subSNat` d1
      in  f s' y (go s' ys)
{-# NOINLINE dfold #-}

I get:

src/Clash/Sized/Vector.hs:1973:11: error:
    • Could not deduce: (n1 GHC.TypeNats.<=? (k - 1)) ~ 'True
        arising from a use of ‘f’
      from the context: n <= k
        bound by the type signature for:
                   go :: forall (n :: Nat). (n <= k) => SNat n -> Vec n a -> p @@ n
        at src/Clash/Sized/Vector.hs:1969:5-62
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   Cons :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
                 in an equation for ‘go’
        at src/Clash/Sized/Vector.hs:1971:11-40
    • In the expression: f s' y (go s' ys)
      In the expression: let s' = s `subSNat` d1 in f s' y (go s' ys)
      In an equation for ‘go’:
          go s (y `Cons` (ys :: Vec (n - 1) a))
            = let s' = s `subSNat` d1 in f s' y (go s' ys)
    • Relevant bindings include
        s' :: SNat n1 (bound at src/Clash/Sized/Vector.hs:1972:11)
        xs :: Vec k a (bound at src/Clash/Sized/Vector.hs:1967:13)
        f :: forall (l :: Nat).
             (l <= (k - 1)) =>
             SNat l -> a -> (p @@ l) -> p @@ (l + 1)
          (bound at src/Clash/Sized/Vector.hs:1967:9)
        dfold :: Proxy p
                 -> (forall (l :: Nat).
                     (l <= (k - 1)) =>
                     SNat l -> a -> (p @@ l) -> p @@ (l + 1))
                 -> (p @@ 0)
                 -> Vec k a
                 -> p @@ k
          (bound at src/Clash/Sized/Vector.hs:1967:1)
     |
1973 |       in  f s' y (go s' ys)
     |           ^^^^^^^^^^^^^^^^^

i.e. I cant convince it that n1 + 1 <= k implies n1 <= k - 1.

[christiaanb]

Okay, if I add:

subMonotone1 :: forall a b c. (a <= b, KnownNat (a - c), KnownNat (b - c)) :- (a - c <= b - c)

then I can implement it:

dfold :: forall p k a . KnownNat k
      => Proxy (p :: TyFun Nat Type -> Type) -- ^ The /motive/
      -> (forall l . (l <= k - 1) => SNat l -> a -> (p @@ l) -> (p @@ (l + 1)))
      -- ^ Function to fold.
      --
      -- __NB__: The @SNat l@ is __not__ the index (see (`!!`)) to the
      -- element /a/. @SNat l@ is the number of elements that occur to the
      -- right of /a/.
      -> (p @@ 0) -- ^ Initial element
      -> Vec k a -- ^ Vector to fold over
      -> (p @@ k)
dfold _ f z xs = go (snatProxy (asNatProxy xs)) xs
  where
    go :: forall n . (n <= k) => SNat n -> Vec n a -> (p @@ n)
    go _ Nil                        = z
    go s@SNat (y `Cons` (ys :: Vec (n - 1) a)) =
      let s' = s `subSNat` d1
      in  case subMonotone1 @n @k @1 of
            Sub Dict -> f s' y (go s' ys)

[IchiroKawashima]

My implementation is like that:

dfold' :: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a
        . (KnownNat k)
       => Proxy p
       -> (  forall (l :: Nat)
           . (KnownNat l, l <= k - 1)
          => SNat l
          -> a
          -> p @@ l
          -> p @@ (l + 1)
          )
       -> (p @@ 0)
       -> Vec k a
       -> (p @@ k)
dfold' Proxy f z = go
  where
    go :: forall (n :: Nat) . (KnownNat n, n <= k) => Vec n a -> p @@ n
    go Nil           = z
    go (y `Cons` ys) = f SNat y (go ys)
{-# NOINLINE dfold' #-}

[IchiroKawashima]

That doesn't require a new axiom.

[christiaanb]

Ah, right... that actually only works because there's a bug in the released version of the ghc-typelits-natnormalise plugin: https://github.com/clash-lang/ghc-typelits-natnormalise/issues/34

the master branch contains this fix: https://github.com/clash-lang/ghc-typelits-natnormalise/pull/35/files, and then your version will no longer compile. When I use your implementation of dfold with the updated plugin I get the same error as I got earlier:

src/Clash/Sized/Vector.hs:1973:24: error:
    • Could not deduce: (n1 GHC.TypeNats.<=? (k - 1)) ~ 'True
        arising from a use of ‘f’
      from the context: (KnownNat n, n <= k)
        bound by the type signature for:
                   go :: forall (n :: Nat). (KnownNat n, n <= k) => Vec n a -> p @@ n
        at src/Clash/Sized/Vector.hs:1971:5-71
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   Cons :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
                 in an equation for ‘go’
        at src/Clash/Sized/Vector.hs:1973:9-19
    • In the expression: f SNat y (go ys)
      In an equation for ‘go’: go (y `Cons` ys) = f SNat y (go ys)
      In an equation for ‘dfold’:
          dfold Proxy f z
            = go
            where
                go :: forall (n :: Nat). (KnownNat n, n <= k) => Vec n a -> p @@ n
                go Nil = z
                go (y `Cons` ys) = f SNat y (go ys)
    • Relevant bindings include
        ys :: Vec n1 a (bound at src/Clash/Sized/Vector.hs:1973:18)
        f :: forall (l :: Nat).
             (KnownNat l, l <= (k - 1)) =>
             SNat l -> a -> (p @@ l) -> p @@ (l + 1)
          (bound at src/Clash/Sized/Vector.hs:1969:13)
        dfold :: Proxy p
                 -> (forall (l :: Nat).
                     (KnownNat l, l <= (k - 1)) =>
                     SNat l -> a -> (p @@ l) -> p @@ (l + 1))
                 -> (p @@ 0)
                 -> Vec k a
                 -> p @@ k
          (bound at src/Clash/Sized/Vector.hs:1969:1)
     |
1973 |     go (y `Cons` ys) = f SNat y (go ys)
     |                        ^^^^^^^^^^^^^^^^

[IchiroKawashima]

Oh, but I could compile the functn even with your implementation in my environment.

[IchiroKawashima]

Okay. I understand.

[adamwalker]

This feature would also be quite useful to me as well. I've needed it in the past as I explained (poorly) here: https://groups.google.com/forum/#!topic/clash-language/O5_l8H6nQKY

[TheZoq2]

I think I have run into the same issue and wanted to try the subMonotone1 thing that @christiaanb posted, however, my haskell knowledge was exceeded long ago with this project so I can't quite figure out how to use it (or even if it's supposed to be useable)

Just adding the code to my own haskell file makes it complain about lacking an accompanying binding, and I can't quite figure out what the binding should be.

[IchiroKawashima]

@TheZoq2 I'm using the following code as a temporary measure.

import           Data.Constraint
import           GHC.TypeLits
import           Unsafe.Coerce

axiom :: forall a b . Dict (a ~ b)
axiom = unsafeCoerce (Dict @(a ~ a))

subMonotone1 :: forall a b c . (a <= b, c <= a) :- (a - c <= b - c)
subMonotone1 = Sub axiom

The code is similar to other axioms defined in Data.Constraint.Nat.

[TheZoq2]

I'm getting this error when I try that:

dtypefoldweird.hs:73:17: error:
    * Couldn't match type `c0 <=? a0' with `c <=? a'
      Expected type: (a <= b, c <= a) :- ((a - c) <= (b - c))
        Actual type: (a0 <= b0, c0 <= a0) :- ((a0 - c0) <= (b0 - c0))
      NB: `<=?' is a non-injective type family
      The type variables `c0', `a0' are ambiguous
    * In the ambiguity check for `subMonotone1'
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        subMonotone1 :: forall a b c. (a <= b, c <= a) :- (a - c <= b - c)
   |
73 | subMonotone1 :: forall a b c . (a <= b, c <= a) :- (a - c <= b - c)
   |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I tried following the compilers advice and added AllowAmbiguousTypes but now I get this error:

dtypefoldweird.hs:75:20: error:
    * Couldn't match kind `Type' with `Bool'
      When matching types
        b0 :: Type
        'True :: Bool
      Expected type: Dict (((a - c) <=? (b - c)) ~ 'True)
        Actual type: Dict (a0 ~ b0)
    * In the first argument of `Sub', namely `axiom'
      In the expression: Sub axiom
      In an equation for `subMonotone1': subMonotone1 = Sub axiom
   |
75 | subMonotone1 = Sub axiom
   |                    ^^^^^

Do I need some more language features or something?

[leonschoorl]

Try enabling PolyKinds

[TheZoq2]

Thanks, that does seem to have done something, but I'm still having trouble:

DFold_.hs:44:25: error:
    * Could not deduce: (n1 <=? (k - 1)) ~ 'True
        arising from a use of `f'
      from the context: n <= k
        bound by the type signature for:
                   go :: forall (n :: Nat). (n <= k) => SNat n -> Vec n a -> p @@ n
        at DFold_.hs:39:5-62
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   Cons :: forall b (n :: Nat). b -> Vec n b -> Vec (n + 1) b,
                 in an equation for `go'
        at DFold_.hs:41:16-45
      or from: (n - 1) <= (k - 1)
        bound by a pattern with constructor:
                   Dict :: forall (a :: Constraint). a => Dict a,
                 in a case alternative
        at DFold_.hs:44:17-20
    * In the expression: f s' y (go s' ys)
      In a case alternative: Sub Dict -> f s' y (go s' ys)
      In the expression:
        case subMonotone1 @n @k @1 of { Sub Dict -> f s' y (go s' ys) }
    * Relevant bindings include
        s' :: SNat n1 (bound at DFold_.hs:42:11)
        xs :: Vec k a (bound at DFold_.hs:37:14)
        f :: forall (l :: Nat).
             (l <= (k - 1)) =>
             SNat l -> a -> (p @@ l) -> p @@ (l + 1)
          (bound at DFold_.hs:37:10)
        dfold_ :: Proxy p
                  -> (forall (l :: Nat).
                      (l <= (k - 1)) =>
                      SNat l -> a -> (p @@ l) -> p @@ (l + 1))
                  -> (p @@ 0)
                  -> Vec k a
                  -> p @@ k
          (bound at DFold_.hs:37:1)
   |
44 |             Sub Dict -> f s' y (go s' ys)
   |                         ^^^^^^^^^^^^^^^^^

For reference: this is the full code I have https://gist.github.com/TheZoq2/03c4a25c09e1ad2cb4fa48a18074d76b

[IchiroKawashima]

The program could be compiled in my environment.

I'm using the latest version of GHC plugin pulled from github. The release version of the plugin has an issue as @christiaanb mentioned and the issue might be related to your problem.

Try using latest version of ghc-typelits-natnormalise.

[leonschoorl]

When we do this in clash-prelude, we should add similar constraints to smap and vfold.

[DigitalBrains1]

2686 does this for dfold and smap, but not the others (dtfold, vfold).