伊德里斯 - 矢量队列和重写规则

我想实现像在伊德里斯功能队列，但它携带在类型元素的数目 - 如Queue ty n m (n+m)其中n是一个Vect n ty元素的数量，m是第二个元素Vect m ty，而(n+m)是总元素。伊德里斯 - 矢量队列和重写规则

的问题是，我遇到了问题与操纵这些尺寸为隐式参数时应用重写规则：

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作品，但bottom没有。看起来我需要提供plusZeroRightNeutral和plusRightSuccRight重写，但我不确定在哪里放置这些内容，或者是否有其他选项。以下是错误消息：

错误上的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)

错误上的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

单独的大小告诉我，当我需要旋转两Vect s，整体大小告诉我什么时候我有一个空的或非空的Queue，所以如果可能的话我想跟踪所有的信息。

来源

2016-12-16 nomicflux

作为注意，我不会将'front' /'back'大小添加到该类型，只是总大小;我认为前者是一个应该从客户端代码隐藏的实现/表示细节。 – Cactus

@Cactus：我一直在把我的代码移动到那个格式，所以我只需要'Queue ty k'，其中'MkQueue'中的'k'仍然是'（n + m）'， 'Vect's，因为这是一个不变的我想保证。不过，我的问题是，我不能拉'{N}'和'{M}'在正确的地方implicits为'top'和'这里bottom'。仍然在这个问题上.... – nomicflux

相关：[总实时持久队列]（http://stackoverflow.com/questions/36611533/total-real-time-persistent-queues）。 – user3237465

解决这个问题的一种可能的方法是破坏n以及。这一次，伊德里斯的理解是，最后一个参数不为零，它基本上是抱怨：

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

作为一个方面说明，我建议让top功能合计：

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

来源

2016-12-16 16:10:50

优秀 - 完美工作，解决了问题，关于总体的说明也很有用。谢谢！ – nomicflux

伊德里斯 - 矢量队列和重写规则

回答

相关问题