[Agda] Re: [Haskell-cafe] Signature for non-empty filter

[Henning Thielemann]

On Tue, 5 Feb 2008, Dan Licata wrote:

> [CC'ed to the agda mailing list as well]
>
> On Feb05, Henning Thielemann wrote:
> >
> > Is Haskell's type system including extensions strong enough for describing
> > a function, that does not always return a trivial value? E.g.
> >    (filter (\x -> x==1 && x==2))
> >   will always compute an empty list. Using an appropriate signature for
> > the function it shall be rejected at compile time, because it is probably
> > a mistake - probably (filter (\x -> x==1 || x==2) xs) was meant. I assume
> > that the type must contain somehow an example input for which the function
> > value is non-trivial. If Haskell's type system is not strong enough, what
> > about dependently typed languages like Cayenne or Epigram? (I know,
> > theorem provers have no problem with such types.)
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
>
> You can definitely do this with dependent types.  Here's a way to do it
> in Agda 2:

Thanks for your detailed answer! I don't fully understand the Agda code,
but I record that there is another system which allows such kind of types.
Now, 'filter' was a particular example where the type constraint can be
reformulated as constraint on the element test 'f'.  However there might
be a composed function like
  stupidFilter = filter odd . map (2*)
 I assume that Agda lets me forbid such functions by properly designed
types, too.