[Haskell-cafe] Signature for non-empty filter
Dan Licata
drl at cs.cmu.edu
Wed Feb 6 19:25:45 EST 2008
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
More information about the Haskell-Cafe
mailing list