1

I'm trying to implement something like a functional queue in Idris, but which carries the number of elements in the type - such as Queue ty n m (n+m) where n is the number of elements in one Vect n ty, m is the elements in a second Vect m ty, and (n+m) is the total elements.

The problem is, I'm running into problems with applying rewrite rules when manipulating these sizes as implicit arguments:

module Queue

import Data.Vect as V

data Queue : Type -> Nat -> Nat -> Nat -> Type where
    mkQueue : (front : V.Vect n ty)
           -> (back : V.Vect m ty)
           -> Queue ty n m (n + m)

%name Queue queue

top : Queue ty n m (S k) -> ty
top {n = S j} {m} {k = j + m} (mkQueue front back) =
    V.head front
top {n = Z} {m = S j} {k = j} (mkQueue front back) =
    V.head $ V.reverse back

bottom : Queue ty n m (S k) -> ty
bottom {m = S j} {n} {k = n + j} (mkQueue front back) = 
    ?some_rewrite_1 (V.head back)
bottom {m = Z} {n = S j} {k = j} (mkQueue front back) = 
    ?some_rewrite_2 (V.head $ V.reverse front)

top works but bottom does not. It would appear that I somehow need to supply plusZeroRightNeutral and plusRightSuccRight rewrites, but I'm not sure where to put those, or whether there might be another option. Here are the error messages:

Error on first line of bottom:

         Type mismatch between
                 Queue ty n (S j) (n + S j) (Type of mkQueue front back)
         and
                 Queue ty n (S j) (S (n + j)) (Expected type)

         Specifically:
                 Type mismatch between
                         plus n (S j)
                 and
                         S (n + j)

Error on second line of bottom:

         Type mismatch between
                 Queue ty (S j) 0 (S j + 0) (Type of mkQueue front back)
         and
                 Queue ty (S j) 0 (S j) (Expected type)

         Specifically:
                 Type mismatch between
                         plus (S j) 0
                 and
                         S j

The individual sizes tell me when I need to rotate the two Vects, and the overall size tells me when I have an empty vs. non-empty Queue, so I do want to track all the information if possible.

Benjamin Hodgson
  • 42,952
  • 15
  • 108
  • 157
nomicflux
  • 45
  • 6
  • 1
    As a remark, I wouldn't add the `front`/`back` size to the type, just the total size; I think the former is an implementation/representation detail that should be hidden from client code. – Cactus Dec 19 '16 at 03:06
  • @Cactus: I've been moving my code over to that format, so that I would just have `Queue ty k`, where `k` in `MkQueue` is still `(n + m)` based on the sizes of the `Vect`s since that's an invariant I want to guarantee. However, then the problem I have is that I can't pull in `{n}` and `{m}` as implicits in the right place for `top` and `bottom` here. Still working on that issue.... – nomicflux Dec 19 '16 at 19:41
  • Related: [Total real-time persistent queues](http://stackoverflow.com/questions/36611533/total-real-time-persistent-queues). – effectfully Jan 02 '17 at 15:56

1 Answers1

2

One possible way of solving this problem is to destruct n as well. This time Idris understands that the last argument is not zero, which it is basically complaining about:

total
bottom : Queue ty n m (S k) -> ty
bottom {m = S m} {n = S n} (MkQueue _ back) = V.head back
bottom {m = S m} {n = Z}   (MkQueue _ back) = V.head back
bottom {m = Z}   {n = S n} (MkQueue front _) = V.head $ V.reverse front
bottom {m = Z}   {n = Z}   (MkQueue _ _) impossible

As a side note, I'd suggest to make the top function total:

total
top : Queue ty n m (S k) -> ty
top {n = S n}           (MkQueue front _) = V.head front
top {n = Z}   {m = S m} (MkQueue _ back) = V.head $ V.reverse back
top {n = Z}   {m = Z}   (MkQueue _ _) impossible
Anton Trunov
  • 15,074
  • 2
  • 23
  • 43