HVect'in tüm alt boyutları nasıl belirlenir?

Question

HVect'un tüm alt boyutlarını HVect olarak belirlemek istiyorum.

Örnek:

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]] ] 

Benim yaklaşım şöyle görünür:

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

ama doğru subDimHVect ve subDimHVect' yazmayı bilmiyorum. Uygulama güzel gibi gözüküyor: Örnek

Manuel Hesaplama:

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]]] 

Ben İdris ve bağımlı türleri için oldukça yeni. Eksik tip imzaları bulmak için biraz yardım isterim.

Düzenleme: Ben de (definition of reverse) türü çözemedim rağmen yazmak daha kolay olabilir başka bir yaklaşım bulundu: Örnek

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

Manuel Hesaplama (kullanarak ikinci yaklaşım):

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

İlk girişimi:

(subDimensions : {ts : Vect n Type} -> {xs : Vect k Type} -> HVect ts -> HVect xs olduğu gibi) örtük bir argüman olarak ele alınacağını, böylece arayan çıkan HVect nasıl görüneceğini söyleyebiliriz. Bu doğru değil. Biz xs yanında (dışarı nasıl bulursanız bu cevabım geçmişini görmek) oluşturabilirsiniz: Ancak

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

, bir

subDimensions : HVect ts -> HVect (dimType ts) 

daha faydalı olacaktır. İkinci denemede takiben,

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

oluşturabilir ve tipi yapısı aşağıdaki şekilde, yardımcı subDimensions' tanımlar: tanımı için (

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

ve sarıcı

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

(hreverse ve vreverse belgesine bakınız here)