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

[Dan Licata]

[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