[Haskell-cafe] Signature for non-empty filter
Dan Licata
drl at cs.cmu.edu
Tue Feb 5 10:44:33 EST 2008
[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:
-- booleans, just like in Haskell:
data Bool : Set where
True : Bool
False : Bool
_||_ : Bool -> Bool -> Bool
False || False = False
_ || _ = True
_&&_ : Bool -> Bool -> Bool
True && True = True
_ && _ = False
not : Bool -> Bool
not True = False
not False = True
-- Now our first use of dependency: we need to turn a boolean value
-- into the proposition that it's true. We do this with a type
-- Check b where only Check True is inhabited; Check False is not
data Check : Bool -> Set where
OK : Check True
-- a function f is satisfiable if there is some input on which it returns true
data Sat {A : Set} : (A -> Bool) -> Set where
Witness : {f : A -> Bool} -> (a : A) -> Check (f a) -> Sat f
-- here's an easy one:
example : Sat (\x -> x || not x)
example = Witness True OK
-- there's no way to prove this one, as each case you'd need
-- a term of type Check False in the empty context
example2 : Sat (\x -> x && not x)
example2 = Witness True {! need a term of type Check False !}
example2 = Witness False {! need a term of type Check False !}
-- Now you can use Sat f as a precondition to filter:
data List (A : Set) : Set where
[] : List A
_::_ : A -> List A -> List A
filter : {A : Set} (f : A -> Bool) -> Sat f -> List A -> List A
filter f sat [] = []
filter f sat (x :: xs) with f x
... | True = x :: (filter f sat xs)
... | False = filter f sat xs
-- Note that the code doesn't use sat at all, so we might as well have
-- written:
stdfilter : {A : Set} -> (A -> Bool) -> List A -> List A
stdfilter f [] = []
stdfilter f (x :: xs) with f x
... | True = x :: (stdfilter f xs)
... | False = stdfilter f xs
fancyfilter : {A : Set} (f : A -> Bool) -> Sat f -> List A -> List A
fancyfilter f _ l = stdfilter f l
That is, the Sat f argument is used only to impose the precondition that
you wanted, and it has no bearing on how filter actually computes.
Of course, the trade-off here is that to call filter you have to cough
up an argument on which the function is satisfiable. I don't know a way
to get the compiler to construct this proof for you, but maybe someone
who has done more dependent programming that I have knows a trick.
You may be able to mimic this using GADTs, but it likely won't be as
direct, because the 'Check (f a)' argument to Sat talks about the very
code that you're passing to filter.
-Dan
More information about the Haskell-Cafe
mailing list