[Agda] lists/vectors (interfacing with untrusted code)

[Nils Anders Danielsson]

On 2012-10-15 14:13, Amr Sabry wrote:
> -- Now I need to take the result of the Haskell function
> -- string2bitlist32 which we know is of length 32 and cast it to 'Vec
> -- Bit 32'. If I can do that then I can write:
>
> main = ainteract (\s -> bitvec2string (swab (CAST (string2bitlist32 s))))
>
> If this approach is viable, I need that CAST.

(With CAST : L.List Bit → Vec Bit 32.)

In this case there is no guarantee that lists and vectors are
represented in the same way—in fact, I suspect that they are not—so CAST
isn't simply a cast.

I believe that the Epic backend compiles lists and vectors to the same
underlying representation.

-- 
/NAD