[Haskell-cafe] Signature for non-empty filter

[Dan Licata]

On Feb06, Henning Thielemann wrote:
> 
> On Tue, 5 Feb 2008, Dan Licata wrote:
> > 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.
> 

I think what you want to say now is not just 

  (filter f l) is type correct when there is some argument on which f
  returns true

but 

  (filter f l) is type correct when there is some *element of l* on
  which f returns true

Here is one way to say this with dependent types:

  data SatBy {A : Set} : (A -> Bool) -> List A -> Set where
    Here  : {f : A -> Bool} {x : A} {xs : List A} -> Check (f x) -> SatBy f (x :: xs)
    There : {f : A -> Bool} {x : A} {xs : List A} -> SatBy f xs -> SatBy f (x :: xs)

  fancyfilter2 : {A : Set} (f : A -> Bool) (l : List A) -> SatBy f l -> List A
  fancyfilter2 f l _ = stdfilter f l

The idea is that SatBy f l proves that there is some element of l on
which (f x) is true.  'Here' says that this is true if (f x) is true on
the head of the list; 'There' says that this is true of (x :: xs) if
it's true of xs.

Of course, now to call fancyfilter2, you need to prove this property of
your f and your l.  You won't be able to do this for 'odd' and 'map (2*)
x', but you would be able to do this for, e.g., 'even' and 'map (2*) xs
where xs is non-nil'.

-Dan