[Agda] lists/vectors

Amr Sabry sabry at cs.indiana.edu
Mon Oct 15 14:06:17 CEST 2012

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? 


> 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

More information about the Agda mailing list