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?