Как определить все субразмеры HVect?

Question

Я хотел бы определить все подразмеры HVect как HVect.

Пример:

import Data.HVect 

myHVect : HVect [Int, String, List Nat] 
myHVect = [42, "text", [1, 2, 3]] 

subDimensions : HVect [ HVect [Int], HVect [Int, String], HVect [Int, String, List Nat] ] 
subDimensions = subDimHVect myHVect 
-- [ [42], [42, "text"], [42, "text", [1, 2, 3]] ] 

Мой подход выглядит следующим образом:

subDimHVect v = subDimHVect' [] [] v 
    where 
    subDimHVect' result _ [] = result 
    subDimHVect' result lastDim (x::xs) = 
     let nextDim = lastDim ++ [x] in 
     subDimHVect' (result ++ [nextDim]) nextDim xs 

, но я не знаю, как правильно ввести subDimHVect и subDimHVect'. Осуществление, кажется, хорошо:

Руководство Расчет примера:

subDimHVect [42, "text", [1, 2, 3]] 
    = subDimHVect' [] [] [42, "text", [1, 2, 3]] 
    = subDimHVect' [[42]] [42] ["text", [1, 2, 3]] 
    = subDimHVect' [[42], [42, "text"]] [42, "text"] [[1, 2, 3]] 
    = subDimHVect' [[42], [42, "text"], [42, "text", [1, 2, 3]]] [42, "text", [1, 2, 3]] [] 
    = [[42], [42, "text"], [42, "text", [1, 2, 3]]] 

Я совершенно новой для Идриса и зависимых типов. Я был бы признателен за помощь в поиске отсутствующих подписей.

Edit: Я нашел другой подход, который может быть проще набрать, хотя я не мог понять тип из любой (definition of reverse):

subDimHVect v = reverse (subDimHVect' (reverse v)) 
    where 
    subDimHVect' [] = [] 
    subDimHVect' (x::xs) = [(x::xs)] ++ (subDimHVect' xs) 

Руководство Расчет примера (с использованием второй подход):

subDimHVect [42, "text", [1, 2, 3]] 
    = reverse (subDimHVect' (reverse [42, "text", [1, 2, 3]])) 
    = reverse (subDimHVect' [[1, 2, 3], "text", 42]) 
    = reverse ([ [[1, 2, 3], "text", 42] ] ++ (subDimHVect' ["text", 42])) 
    = reverse ([ [[1, 2, 3], "text", 42] ] ++ [ ["text", 42] ] ++ (subDimHVect' [42])) 
    = reverse ([ [[1, 2, 3], "text", 42] ] ++ [ ["text", 42] ] ++ [ [42] ] ++ (subDimHVect' [])) 
    = reverse ([ [[1, 2, 3], "text", 42] ] ++ [ ["text", 42] ] ++ [ [42] ] ++ []) 
    = reverse ([ [[1, 2, 3], "text", 42], ["text", 42], [42] ]) 
    = [ [42], [42, "text"], [42, "text", [1, 2, 3]] ] 

Answer 1

Первая попытка:

subDimensions : HVect ts -> HVect xs 

The xs будет рассматриваться как неявный аргумент (как в subDimensions : {ts : Vect n Type} -> {xs : Vect k Type} -> HVect ts -> HVect xs), так что абонент может сказать, как в результате HVect будет выглядеть. Это не правильно. Мы могли бы создать xs вместе (см истории этого ответа, если вы узнаете, как):

subDimensions : HVect {k} ts -> (xs : (Vect k Type) ** HVect xs) 

Однако

subDimensions : HVect ts -> HVect (dimType ts) 

будет более полезным. После вашей второй попытки, мы можем создать

dimType : Vect k Type -> Vect k Type 
dimType [] = [] 
dimType (x :: xs) = (HVect (vreverse (x::xs))) :: dimType xs 

и в соответствии со структурой типа, определим вспомогательные subDimensions':

subDimensions' : HVect ts -> HVect (dimType ts) 
subDimensions' [] = [] 
subDimensions' (x :: xs) = (hreverse (x :: xs)) :: subDimensions' xs 

и обертку

subDimensions : HVect ts -> HVect (vreverse (dimType (vreverse ts))) 
subDimensions xs = hreverse $ subDimensions' $ hreverse xs 

(для определения от hreverse и vreverse см. here)