Darren New wrote:

>> Logically speaking, given a function and a list, you can either do any 
>> of the following:
> 
> Right. I was asking what code it generated given a signature.

And I was just agreeing that more than one function has that type. 
However, the website says:



The theorem generated for functions of the type

f :: forall a . [a] -> (a -> Bool) -> [a]

in the sublanguage of Haskell with no bottoms is:

forall t1,t2 in TYPES, R in REL(t1,t2).
  forall (x, y) in lift{[]}(R).
   forall p :: t1 -> Bool.
    forall q :: t2 -> Bool.
     (forall (z, v) in R. p z = q v)
     ==> ((f x p, f y q) in lift{[]}(R))

The structural lifting occurring therein is defined as follows:

lift{[]}(R)
   = {([], [])}
   u {(x : xs, y : ys) |
        ((x, y) in R) && ((xs, ys) in lift{[]}(R))}

Reducing all permissible relation variables to functions yields:

forall t1,t2 in TYPES, g :: t1 -> t2.
  forall x :: [t1].
   forall p :: t1 -> Bool.
    forall q :: t2 -> Bool.
     (forall y :: t1. p y = q (g y))
     ==> (map g (f x p) = f (map g x) q)



I have absolutely *no clue* what the hell any of that means. But try it 
yourself here:

http://linux.tcs.inf.tu-dresden.de/~voigt/cgi-bin/ft/ftonline.cgi

>>> Do you actually have algebraic datatypes in Haskell? Kewl.
>>
>> Um... yes?
>>   data Either x y = Left x | Right y
> 
> Oh, OK. Can you do something more complex, like say a stack?
> 
> Hmmm... Maybe essentially all user types in Haskell are ADTs, and I just 
> never thought of it that way before?

Indeed, all Haskell types are ADTs. Except things like integers, 
arguably. OTOH, you could claim that Integer is defined as

   data Integer = 1 | 2 | 3 | 4 | ...

As for "like say a stack", I'm not really sure what you mean.

>> Much like the "Haskell doesn't need a debugger because programs work 
>> correctly first time". Until we got a debugger... and now it's "hey, 
>> we have a debugger!"
> 
> Oddly enough, a lot of projects created by nerds are like that.

I wonder if this is why Linux doesn't "need" a defrag tool?

Post a reply to this message