Any plans on compiler-,macro (lib name) like functions?

[commander-trashdin]

Such as extraction various information from types (contained element type, dimensions, ranges, etc) and providing something like default value? I can certainly help with both.

[Bike]

do you have an API in mind? i think this is a bit more involved than it looks. for example if you have a type like (and (cons integer) (satisfies foo)), you can't exactly determine the car type, though of course you can get an upper bound on it (integer). Or, for a type like (or (cons integer) (array integer)) it may be useful to know that the car may be undefined, whereas it would always be defined on just (cons integer). (Well, I guess not, since nil is a subtype. Maybe upper and lower bounds could be good.)

eta: There's also the question of what such things mean with how CL functions work. For example, if you want to know the type of a form (car x), that can be existent if x is of type null, since (car nil) = nil.

My vague plan for this was to export a funcall or apply operator, that would take a function type and a list of argument types and return the type of the result. But in general this could be a quite arbitrary computation, e.g. to get a good answer with arithmetic functions you would want to carry out interval arithmetic.

[commander-trashdin]

Not talking about inference for now. But ye I don't think you can always define default value, and you cannot always extract stuff. Sometimes you can tho, and this is when it's useful.

Btw I am now using this as a backend (and digikar added it to his trivial type form) so at least I m going to support it.

I'll sketch something and get back to you tomorrow.

[commander-trashdin]

For now we are doing something like this

https://github.com/digikar99/trivial-form-type

[commander-trashdin]

Also, it's really a shame that you decided to go with upgrading array element types, that doesn't affect efficiency but hinders type inference even more. You mind maybe changing it back to precise types? I think any compiler that does upgrades will do them anyway.

[Bike]

I wouldn't mind keeping information about the declared element type around, but I can't just ignore upgrading. The type system is defined such that if two arrays element types upgrade to the same thing, the array types are the same (so subtypep is true both ways).

To be clear, while this is intended to be used by compilers, it is also intended to implement the cl:typep and cl:subtypep functions generally. I won't do things that break the standard there. Knowing the declared element type would affect questions like "what is the type of (aref the-array ...)", rather than the results of typep or subtypep.

[commander-trashdin]

I see your point. Maybe having an upgraded-p slot (with either nil or upgrade result) makes sense? This way original info can be preserved.

[Bike]

I can just add another slot, so we have one for the declared type and one for the upgraded one. I think that is how SBCL's ctype system works, and that's the best type system in Lisp so I tend to go with what it does. And I suppose the declared type should actually be parsed into a ctype, since it represents the types of values, unlike the upgraded array element type which pretty much just indicates a storage class. I can do the same for complex part types. And maybe I could put a flag on this for people who doesn't want declared element types to be parsed.

Not talking about inference for now.

If all you want is low level accessors exported, for use building a higher level inference mechanism, I can do that sure. This would be "low level" in the sense that e.g. (or null (cons integer)) would be a union type not a cons ctype, so the "car" accessor would not work. Then a higher level inference, like "if x is of type y, what is the type of (car x)?" could be written (outside of this library) something like

(defgeneric car-ctype (ctype))
(defmethod car-ctype ((ctype ctype:ctype)) (ctype:top)) ; ignorance
(defmethod car-ctype ((ctype ctype:cclass)) (ctype:bot))
(defmethod car-ctype ((ctype ctype:conjunction))
  (apply #'ctype:conjoin (mapcar #'car-ctype (ctype:junction-ctypes ctype))))
(defmethod car-ctype ((ctype ctype:disjunction))
  (apply #'ctype:disjoin (mapcar #'car-ctype (ctype:junction-ctypes ctype))))
(defmethod car-ctype ((ctype ctype:ccons)) (ctype:ccons-ccar ctype))
(defmethod car-ctype ((ctype ctype:range)) (ctype:bot))
(defmethod car-ctype ((ctype ctype:fpzero)) (ctype:bot))
(defmethod car-ctype ((ctype ctype:ccomplex)) (ctype:bot))
(defmethod car-ctype ((ctype ctype:cmember))
  (apply #'ctype:conjoin
         (loop for mem in (ctype:cmember-members ctype)
               collect (typecase mem
                         (null (ctype:cmember nil))
                         (cons (ctype:cmember (car mem)))
                         (t (ctype:bot))))))
(defmethod car-ctype ((ctype ctype:carray)) (ctype:bot))
(defmethod car-ctype ((ctype ctype:charset)) (ctype:bot))
(defmethod car-ctype ((ctype ctype:cfunction)) (ctype:bot))

The only problem here is that some of this is kind of ugly to deal with... e.g. I consider fpzero to be an implementation detail.

[commander-trashdin]

Ye, so I was trying to deal with problems with compiler-macro which cannot extract array element type for something like (and (array fixnum (*)) t) even though it's trivial. Not even mentioning some other more complicated cases.

For form-type, if you have time to look at trivial-form-type that I linked above....I said "not talking about inference" because I need all the proper extractors before I can do proper inferrers.

[commander-trashdin]

By the way, I like your impl, I just am unsure if having bottom type returned is better than error.

[Bike]

Error? What would signal an error? My little example there? That's so that if you give it a type like (or (cons integer) array) it works on each element of the junction to get integer and nil, and then disjoins those into the correct answer, integer. Perfectly legitimate forms can have a type of nil as well, such as calls to error, so I figure whatever higher level mechanism should be the one determining whether to treat bottom as an error.

And yeah I looked at your code a bit. You are worried about cases like intelligently inferring the type of (aref (the (array cons) a) ...). The trick is that I don't think that an extractor that only works on array ctypes is what you need. I mean, you could use it, but you'd get needlessly imprecise answers for even fairly simple question.

A more complicated case would be interval arithmetic. Say you have (+ x y), and you know x is an (or (integer 3 7) cons (integer 12 246)) and y is an (integer 4 15). Then (+ x y) must be an (or (integer 7 22) (integer 16 261)); but you can't just work with range ctypes, since the type of x will be a junction ctype in this system. Of course you'd probably also want to know that after that call x can no longer be a cons, so maybe it could be expected that you take the intersection with a numerical type first...

More babbling: there's also the possibility of dealing with certain kinds of type specially, in ways that are kind of orthogonal to the type lattice. For example, in your inferrer there you use constantp in the make-array inference, but what SBCL does is recognize "constant" types, i.e. eql types essentially, and work on those specially. That's probably better for the inference overall, but now you're worried about the actual form of the type, and not just how it behaves as a set.

Yeah definitely babbling. Sorry. Tell you what, how about I just export these simple accessors and we figure out what to do from there. Especially it would be good to know what would make your inference code most convenient to write.

[commander-trashdin]

Nvm my comment about the error, it wasn't smart)

Interval arithmetic is hard, but there's a ...sort of a trick to it -- we hooked into sbcl inference in a way, and so sbcl does intervals for us (at least for now). The other compilers -- we may support as well. And of course in the future maybe we'll do intervals ourselves.

Tell you what, how about I just export these simple accessors and we figure out what to do from there.

Deew it.

[Bike]

If you're using SBCL's types, you don't really need this library, do you?

[commander-trashdin]

We do, because:

1. sbcl actually doesn't do all the inference we need and want.
2. this is not supposed to be sbcl only(it is cltl2 only though) and while our impl differs on sbcl, it still works on other impls as well.
3. Basically on sbcl we just do a bit more type inference by abusing its system -- which is nice, but doesn't define anything.

[Bike]

alright.

threw in some exports. If you figure out a better interface I would love to hear about it. I'll do the element type stuff next.