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.

[commander-trashdin]

One of the things I m thinking about is that... If I do the type specialized structures the way I do them right now that means that for (map fixnum) I basically generate a unique class, sort of map-of-fixnum. However I would also want to make it so map of fixnums is subtype of map of numbers. While they are just different unrelated classes. You think that's possible? Because I don't want to just hardcode it into ctype:subtypep.

[Bike]

I was thinking about generalizing the cons type for arbitrary type constructors, which I think would cover what you're talking about? The map type constructor would have the same sort of relations that cons types do, i.e. (map nil) is nil, (map x) is a subtype of (map y) iff x is a subtype of y, (map x) is a proper subtype of T, etc.

[commander-trashdin]

It's just that under the hood they are completely unrelated classes with dumb generated names. So they will be ...like, not subtypes if we were to treat them as just classes.

[Bike]

Oh, the idea has always been to define custom ctype classes for that kind of thing. The class structure doesn't need to be involved. This is in the same way that while all conses have the same class, there's an infinite constellation of cons types.

[commander-trashdin]

If you do and push several extractors -- I can look at them and help with the rest.

[commander-trashdin]

https://github.com/alex-gutev/cl-form-types

Talking about API as well as some code to look at/borrow from

[commander-trashdin]

Oh and it would be nice if we could have a more reliable communication channel than this. I tried to find you on IRC but to no avail so far.

[Bike]

I'm on Freenode. #sicl channel would probably be best. I'm not on 24/7 but I read logs.

[Bike]

full on structure types like i was thinking of are going to be pretty involved since there's some exponential blowup. with just one field it should be pretty easy though. With your maps...

(defclass cmap (ctype)
  ((%element-ctype :initarg :element-ctype :reader element-ctype)))

(defun cmap (element-ctype)
  (if (bot-p element-ctype)
      element-ctype
      (make-instance 'cmap :element-ctype element-ctype)))

(defmethod ctypep ...)
(defmethod subctypep ((ct1 cmap) (ct2 cmap))
  (subctypep (element-ctype ct1) (element-ctype ct2)))
(defmethod ctype= ((ct1 cmap) (ct2 cmap))
  (ctype= (element-ctype ct1) (element-ctype ct2)))
(defmethod disjointp ((ct1 cmap) (ct2 cmap))
  (disjointp (element-ctype ct1) (element-ctype ct2)))
(defmethod conjointp ((ct1 cmap) (ct2 cmap)) (values nil t))
(defmethod cofinitep ((ct cmap)) (values nil t))
(defmethod negate ((ct cmap))
  (let ((nect (negate (element-ctype ct))))
    (if (bot-p nect)
        (call-next-method)
        (disjunction (negation (cmap (top))) (cmap nect)))))
(defmethod conjoin/2 ((ct1 cmap) (ct2 cmap))
  (cmap (conjoin (element-ctype ct1) (element-ctype ct2))))
(defmethod disjoin/2 ((ct1 cmap) (ct2 cmap))
  (cmap (disjoin (element-ctype ct1) (element-ctype ct2))))
(defmethod subtract ((ct1 cmap) (ct2 cmap))
  (cmap (subtract (element-ctype ct1) (element-ctype ct2))))
(defmethod unparse ...)

plus a couple methods to make them work correctly with the classes. I guess that isn't so bad, but some of this would need to be exported

[commander-trashdin]

If I had something like this, that would cover 95% of all usages in my lib so far.

(defgeneric container-element-ctype (ctype))
(defmethod container-element-ctype ((ctype ctype::ctype)) (ctype::top)) ; ignorance
(defmethod container-element-ctype ((ctype ctype::cclass)) (ctype::bot))
(defmethod container-element-ctype ((ctype ctype::conjunction))
  (apply #'ctype::conjoin (mapcar #'container-element-ctype (ctype::junction-ctypes ctype))))
(defmethod container-element-ctype ((ctype ctype:disjunction))
  (apply #'ctype:disjoin (mapcar #'container-element-ctype (ctype:junction-ctypes ctype))))
(defmethod container-element-ctype ((ctype ctype:cvalues))
  (container-element-ctype (first (ctype:cvalues-required ctype))))
(defmethod container-element-ctype ((ctype ctype:ccons)) (ctype:bot))
(defmethod container-element-ctype ((ctype ctype:range)) (ctype:bot))
(defmethod container-element-ctype ((ctype ctype:fpzero)) (ctype:bot))
(defmethod container-element-ctype ((ctype ctype:ccomplex)) (ctype:bot))
(defmethod container-element-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 container-element-ctype ((ctype ctype:carray)) (ctype:carray-eaet ctype))
(defmethod container-element-ctype ((ctype ctype:charset)) (ctype:bot))
(defmethod container-element-ctype ((ctype ctype:cfunction)) (ctype:bot))



(defgeneric container-dims (ctype))
(defmethod container-dims  ((ctype ctype:ctype)) (ctype:top)) ; ignorance
(defmethod container-dims ((ctype ctype:cclass)) (ctype:bot))
(defmethod container-dims ((ctype ctype:conjunction))
  (apply #'ctype:conjoin (mapcar #'container-dims (ctype:junction-ctypes ctype))))
(defmethod container-dims ((ctype ctype:cvalues))
  (container-dims (first (ctype:cvalues-required ctype))))
(defmethod container-dims ((ctype ctype:disjunction))
  (apply #'ctype:disjoin (mapcar #'container-dims (ctype:junction-ctypes ctype))))
(defmethod container-dims ((ctype ctype:ccons)) (ctype:bot))
(defmethod container-dims((ctype ctype:range)) (ctype:bot))
(defmethod container-dims ((ctype ctype:fpzero)) (ctype:bot))
(defmethod container-dims ((ctype ctype:ccomplex)) (ctype:bot))
(defmethod container-dims ((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 container-dims ((ctype ctype:carray)) (ctype:carray-dims ctype))
(defmethod container-dims ((ctype ctype:charset)) (ctype:bot))
(defmethod container-dims ((ctype ctype:cfunction)) (ctype:bot))

[commander-trashdin]

Thinking about it, what should be the default for dimensions on type that do not have them...Dimensions are not a type, so the default probably should not be bottom as well, but what?....

[Bike]

I'm not sure if this is something that belongs in this library, or rather would be a use of it. Relatedly, I think the answer to your container dims question is that it depends on what you're doing with the information.

[commander-trashdin]

Fair enough, I guess I ll create my own then)

What I'm doing is well....I use it. I suppose nil could be the option for number parameterization.

[Bike]

Of course you use it. How you use it determines what you want, no? In some applications you might want to distinguish between "no information" and "could have any dimensions, and in others you might not, for example.

[commander-trashdin]

https://github.com/lisp-polymorph/introspect-ctype/blob/master/introspect-ctype.lisp

This is bad but I ll make it better. Any suggestions are appreciated.

[Bike]

The dimensions of an array ctype should be normalized to always be a list, so your methods specialized on integers shouldn't be necessary. If you are seeing integers that's a bug on my part