freenode/#sicl - IRC Chatlog
Search
6:37:52
heisig
"The environment object has dynamic extent; the consequences are undefined if the environment object is referred to outside the dynamic extent of the macro expansion function."
6:39:07
heisig
What that means is we should clarify that trucler-native can only work reliably when invoked within the dynamic extent of a macro expansion.
6:52:10
MichaelRaskin
heisig: obviously. A slightly simpler version of native-environment-construction in Agnostic-Lizard could be made to crash because of not respecting dynamic extent.
6:53:05
heisig
I mean, it is not a big problem now that I think about it. Using environments outside of the dynamic extent of the compiler or macroexpander is not something I would want to see in the wild.
6:53:59
heisig
And I already realized that for Cleavir it is enough to support native global environments.
6:54:35
MichaelRaskin
It does sometimes make code slightly more complicated when you have multiple expander dynamic extent to think about, but yeah, not a real problem
7:54:56
beach
Hmm. Baker's paper on SUBTYPEP does not discuss CONS at all. I wonder whether his technique is able to handle that at all.
7:58:28
MichaelRaskin
My default expectation would be that bounded-depth CONS should probably be doable by just running the same algorithm on CAR and CDR. Of course, this doesn't cover the most typical use of CONS, namely lists.
8:00:39
MichaelRaskin
I mean more that «very straightforward extension is exceedingly likely to work»
8:05:31
MichaelRaskin
Given the problem, maybe a modern first-order prover might be an even better idea
8:07:09
MichaelRaskin
There is the middle ground of using something like CSP which is slightly richer than pure SAT and can use more structure while requiring less preprocessing; there is an even more dramatic option of going to SMT (satisfiability modulo theory) to allow a richer variety of integer constraints to be handled.
8:23:13
heisig
Now that I have had a look at the input language of SMT solvers- SMT-LIB, I conclude we absolutely have to use that.
8:24:32
heisig
"Its syntax is similar to that of the LISP programming language. In fact, every expression in this version is a legal S-expression of Common Lisp."
8:27:24
heisig
MichaelRaskin: The current implementations of SUBTYPEP are also underfuzzed - ask Jim Newton :)
8:53:24
beach
Anyway, if someone has some insight as to how to formulate SUBTYPEP as an SMT problem, let me know.
9:01:07
MichaelRaskin
Well, in case of logics, if ∀x A(x)→B(x) is provable, then A is definitely subtype of B, and if ∃x A(x)∧¬B(x) is provable, then A is definitely not a subtype of B
9:02:54
MichaelRaskin
I guess with SMT there is an extra detail that one needs to prevent floating-point arithmetics to be interpreted as integer arithmetics
9:05:04
no-defun-allowed
"All objects that are of type A are of type B" and, well, I don't know how to read the second.
9:05:21
shka_
well, i am not mathematician, but as long as you can represent your subtypes logic as first order logic expressions, it should work
9:28:26
scymtym
i used the SMT-based approach in https://techfak.de/~jmoringe/gradual-set-theoretic-types.html although it doesn't show in those examples
10:52:36
beach
scymtym: Are you saying that you already have an implementation of SUBTYPEP using SMT?
12:42:12
Bike
"CONS types. Only (CONS T T) and variants, as well as (CONS NIL *), etc are strictly supported." well that's a worrying comment
12:43:59
Bike
since it's baker, it tries to give every type a bit vector (or actually a number, but it's treated as a bit vector)
12:44:51
Bike
for a cons type it does that recursively with the car and cdr. if they're both -1 (T) it returns the bit vector for cons. if either is 0 (NIL) it returns 0. otherwise it gives up, which seems to result in subtypep returning NIL NIL
12:48:04
beach
I think Baker's method works for everything except (CONS <t1> <t2>) in the general case.
12:52:46
beach
So it looks to me like Baker's algorithm splits each "leaf type (or set)" into elementary sets that do not overlap, and then the problem becomes equivalent to determining whether a set composed of the union, intersection, and complement of these elementary sets is necessarily the empty set.