Serguey Zefirov wrote:
let (xys : Vec m (Vec n X) ---- transpose xys: Vec n (Vec m X))
Why isn't it possible to use Haskell version of transpose as a boilerplate?
transpose [] = []
transpose ([] : xys) = transpose xys
transpose ((x:xs):xys) = ...
BTW, when I elaborating cases in Epigram, the first case of transpose
xys is a vnil (after rec xys then case xys). And, actually, it makes
sense to return vnil as an aswer. But Epigram colours return of vnil
in brown.
From elaboration information in Epigram buffer I figured out that
first vnil case is a transposition to (Vec m (Vec zero X)) and tried
recursion on m. It gave me two cases for vnil. First vnil (Vec zero
(Vec zero X)) can be transposed into vnil. But second vnil (for result
type Vec (suc m) (Vec zero X)) couldn't elaborate preperly.
Now I am lost for a little bit longer than in previous questions.
0xN is an empty list
Nx0, the result of the transposition, is a list of N empty lists. You
can express this (the value of N...) with vectors/dependent-types, you
know how long it should be, so you can do this.
does that seem right?
