[Agda] lists/vectors

[Amr Sabry]

That would work but it would pollute the Agda code with all these
'runtime' checks.

I would prefer to have one entry point to the Agda code that is unsafe
as far as Agda is concerned but trusted because the user does validation
on the other side.

Is that not a reasonable approach? 

--Amr

> On 2012-10-14 02:45, Amr Sabry wrote:
> > 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.
> 
> One alternative is to do the checking on the Agda side:
> 
>   List Bool → Maybe (Vec Bool 32)
> 
> -- 
> /NAD
>