Search
Sunday, 6th of October 2019, 0:39:07 UTC
1:01:04
saturn2
errors like this (defun foo () (labels ((a (x) (if (< x 5) (a (1+ x)) x))) (the (mod 4) (a 0))))
1:09:53
saturn2
if you go backwards you can prove that a never returns a number less than 5, if you only go forwards you can't
1:10:36
stassats
that doesn't make any sense
1:11:52
stassats
don't know, starting from wrong premises or something?
1:26:38
saturn2
could you explain why sbcl doesn't warn about a type error when compiling that code, but it does with this? (defun foo () (labels ((a (x) (if (< x 5) 5 x))) (the (mod 4) (a 0))))
1:27:39
stassats
because it doesn't derive the type of that function
1:31:52
stassats
(and that (mod 4) wouldn't help it)
1:32:10
stassats
it could be derived as > 5 as it is
1:35:15
saturn2
the (mod 4) is a deliberate error i put there for sbcl to catch
1:36:40
stassats
where are your supposed benefits of backwards type propagation then?
1:37:17
stassats
it would work by going forward, if it were not a recursive function
1:37:36
saturn2
with backwards type propagation, it could work also with the recursion
1:38:24
stassats
backwards from what? backwards how?
1:41:23
stassats
e.g. (defun bar (x) (declare (integer x)) (block nil (tagbody loop (if (< x 5) (incf x) (return x)) (go loop)))) derives as (integer 5)
1:41:58
stassats
by knowing that the only way it's returning is when x is >= 5
1:42:03
stassats
nothing backwards about that
12:31:51
stassats
wonder if it'll be useful to fold (gcd ... 1) to 1
Sunday, 6th of October 2019, 12:39:07 UTC