[Agda] lists/vectors

[Noam Zeilberger]

On Mon, Oct 15, 2012 at 7:06 AM, Amr Sabry <sabry at cs.indiana.edu> wrote:
> 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

I think what you want is an axiom that the result of string2bitlist32
is a list of length 32:

  postulate len32 : (s : S.String) -> length (string2bitlist32 s) == 32

By composing string2bitlist32 with fromList and this equation, you can
then write:

trusted-string2bitlist32 : S.String -> Vector Bool 32
trusted-string2bitlist32 s = subst (Vector Bool) (len32 s) (fromList
(string2bitlist32 s))

where 'subst' is defined in Relation.Binary.PropositionalEquality.Core.

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

I had to do something like this in an Agda development that (for
performance reasons and to make life easier) plugs with Haskell's
primitive arbitrary-precision rational arithmetic: besides the
arithmetic operations themselves, I postulate that the field axioms
hold, trusting GHC not to violate them.

One major limitation that I had to deal with, though, is that I wanted
to run this Haskell code from within Agda in interactive mode, whereas
the current FFI only works for compiled Agda.  My painful solution was
to manually extend Agda's BUILTIN keyword with support for the Haskell
type Rational, addition, multiplication, etc.  I will echo Nisse's
words and suggest that there is a lot of room for improving the FFI.

Noam