#haskell - Tue 1 May 2007 between 01:32 and 01:49

NY Lost Funds



donsright.
[1..] ++ x is _|_
SamB_XPdibblego: well, last ([1..] ++ foo) is _|_, regardless of foo
dibblegoyes I agree and I should have seen it that way
donsif you put a type constraint on '1' it might work .. :-)
(i.e. boundedEnumFrom
dibblegoah yes
donsthen 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.
KorollaryI 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.
donsnah. rules would be enough.
you can code algebraic properties of the api as rewrite rules
so , for example, last (_ ++ [x]) --> x
for bounded types.
KorollaryYes 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.
ddariusdons: Computational Category Theory is implementing CT in ML.
donsyep.
ddariusSome pretty cool things since most of CT is constructive.
KorollaryCoq has CT modules
ddariusdibblego: Because _|_ /= 7
dibblegoddarius, good answer :)
donsdibblego: you're optimisation is this, I think:
{-# RULES
"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
ddariusThat would be a bad thing.
To put one way, a lot of productive things in Haskell == _|_.
sorearddarius: Useful programs as a whole do not evaluate to _|_

Page: 1 8 15 22 29 36 43 50 57 64 71 78 85 92 99 

IrcArchive

NY Lost Funds