[1..] ++ x is _|_
|SamB_XP||dibblego: well, last ([1..] ++ foo) is _|_, regardless of foo|
|dibblego||yes I agree and I should have seen it that way|
|dons||if you put a type constraint on '1' it might work .. :-)|
|dons||then you're just changing the complexity, not the termination|
RULES forall xs y.
last (xs ++ [y]) = y :: Int
so for bounded, strict types, that might be ok.
|Korollary||I think the real reason is that last works on list values, not expressions that can be combined to produce lists. The compiler would have to use a theorem prover.|
|dons||nah. rules would be enough.|
you can code algebraic properties of the api as rewrite rules
so , for example, last (_ ++ [x]) --> x
for bounded types.
|Korollary||Yes you can add axioms. For a general solution you'd need a prover.|
|dons||(don't even have to be strict).|
right. if you wanted your compiler to find these optimisations.
|ddarius||dons: Computational Category Theory is implementing CT in ML.|
|ddarius||Some pretty cool things since most of CT is constructive.|
|Korollary||Coq has CT modules|
|ddarius||dibblego: Because _|_ /= 7|
|dibblego||ddarius, good answer :)|
|dons||dibblego: you're optimisation is this, I think:|
"last/append" forall e (v :: Int).
last ((++) e (v : )) = v
of course, 'e' might still be bottom :-)
so its refining non-terminating programs to terminating ones. ah well
last (undefiend ++ (v :  ) --> v
|sorear||_|_ /= <demons>|
perhaps it should be
|ddarius||That would be a bad thing.|
To put one way, a lot of productive things in Haskell == _|_.
|sorear||ddarius: Useful programs as a whole do not evaluate to _|_|