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

[Amr Sabry]

Hi,

I don't want something of type:

>   (xs : List Bool) -> Vector Bool (length xs) 

I really am looking for something of type:

>   (xs : List Bool) -> Vector Bool 32

More generally how do you guys interface between untrusted code and Agda
code??? 

--Amr

Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com> wrote:

> On Sat, Oct 13, 2012 at 7:45 PM, Amr Sabry <sabry at cs.indiana.edu> wrote:
> > Hi all,
> >
> > Probably a fairly basic question...
> >
> > Say I have an Agda module that works with things of type
> >
> >   Vector Bool 32
> >
> > How does one write a complete program, i.e., an external Haskell
> > wrapper, that interacts with this module? I am thinking of a Haskell
> > wrapper that reads an arbitrary string, checks that the string length is
> > 32, and if so calls the Agda code. This approach requires some
> > function:
> >
> >   (xs : List Bool) -> Vector Bool 32
> 
> I guess you can use the function fromList
> http://www.cse.chalmers.se/~nad/listings/lib-0.6/Data.Vec.html#4403
> instead.
> 
> -- 
> Andrés