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.
12:55:04
beach
And this formula ought to be possible to express as something that can be solved by an SMT solver.
12:56:11
Bike
you can do 3-sat with satisfies types, if subtypep lets them be subtypes of themselves
13:01:13
beach
Now, (CONS <t1> <t2) is a subtype of (CONS <t3> <t4>) if and only if <t1> is a subtype of <t3> and <t2> is a subtype of <t4>, right?
13:02:09
beach
So apparently Baker's method fails to express that as a bunch of elementary non-overlapping sets.
13:02:40
MichaelRaskin
Although that might not be true for some very optimised and case-by-case cons implementations (that also don't seem too reasonable for Lisp)
13:04:05
MichaelRaskin
In principle one could have cons-of-(unsigned-byte 8)-or-null as a special optimised representation that is only used when the type is declared and this special representation is not a subtype of cons-of-number-or-null
13:06:46
MichaelRaskin
Hm. Maybe it is indeed better to have types as values (to be able to provide an axiom for CONS with a quantifier over types)
13:09:11
MichaelRaskin
One can either try to expand CONS before asking FO or SMT solver, or provide an axiom to the solver to deal with CONS.
13:12:01
beach
Hmm, wait! Could one use a recursive invocation of SUBTYPEP to split those occurrences of CONS types into elementary non-overlapping sets?
13:17:08
beach
I should also re-read Jim's dissertation to see whether his algorithm for splitting sets into non-overlapping subsets handles CONS types.
13:20:56
MichaelRaskin
Hopefully yes, but probably without caring about exponential growth (because every part of the algorithm already has this exponential growth)
13:22:53
MichaelRaskin
Of course, we don't know what practical purposes will arise once there is a library with subtypep that works well
13:23:58
beach
Now, in the case where there is exponential growth, would an axiom-based technique behave badly as well?
13:24:26
MichaelRaskin
Depends. Everything from SAT-solvers and up has quite a bit of black magic inside.
13:26:34
MichaelRaskin
In the most general case you can probably model worst-case SAT problem, whatever is the worst case for the chosen tool. And many people believe in SETH, i.e. the worst case for every SAT-solver is exponential.
17:11:21
fiddlerwoaroof
hi, I've been trying to use SICL recently and I've run into a couple issues.
17:12:22
fiddlerwoaroof
1) the README says to start a repl with (repl ee4) which uses an undefined symbol EE4 and calls an undefined function REPL
17:13:31
fiddlerwoaroof
2) When I load sicl-boot-inspector, I get a couple errors: first, I get INSPECT is not external in package CLOUSEAU
17:14:14
fiddlerwoaroof
3) If I fix that (export 'clouseau::inspect (find-package :clouseau)), I get this error: https://github.com/robert-strandh/SICL/issues/145#issuecomment-544271263