libera/#commonlisp - IRC Chatlog
Search
1:04:33
nij_
One thing I find weird about CL type system is the SATISFIES keyword. It doesn't seem to support sane interface. Can I safely assume that the "types" mentioned in CL is not as what other people mean usually?
1:05:50
nij-
Ooops my first message didn't send through: > I've always been confused with the difference between classes and types. Until today, I read [1] which seems to make it click. My summary is that classes are moer about implementation details, while types are more about their interfaces. That's maybe why types support polymorphisms with more sanity. [1]
1:05:51
nij-
https://www.cs.princeton.edu/courses/archive/fall98/cs441/mainus/node12.html#SECTION00043000000000000000
1:08:53
pjb
nij-: first thing to note, is that there's no first class types in Common Lisp (there's no type type). What we have are type DESIGNATORS, mere sexps denoting types.
1:09:51
pjb
nij-: there's a little exception, for classes, since classes are type designators for the set of their instances, so in a way, class objects are first class types, but it's an exceptionnal situation, and #<class foo> is equivalent to foo as type designators.
1:10:17
Bike
nij-: lisp types are different from types in most languages (and e.g. type theory) because they are quite explicitly sets, and moreover sets in naive set theory
1:11:10
pjb
nij-: Well, types in CL forms a lattice. This is not always the case. They represent indeed sets of values, but all types should be sets of values.
1:11:54
pjb
satisfies just takes a predicate. This (satisfies foop) = { x | foop(x) } which is perfectly defined set, therefore a perfectly defined type.
1:13:40
pjb
(defun self-not-included-p (x) (not (member x x))) (self-not-included-p '(a b c)) #| --> t |# (self-not-included-p '#1=(a b #1# d)) #| --> nil |#
1:14:29
pjb
(deftype self-not-included () '(satisfies self-not-included-p)) (values (typep '(a b c) 'self-not-included) (typep '#1=(a b #1# d) 'self-not-included)) #| --> t ; nil |#
1:14:39
nij_
I see. Thanks. I understand those as "CL types are more like sets, which differ from the types in most languages."
1:16:23
pjb
nij_: the trick is that in lisp, it's values that have types, not variables. In languages like C, you declare the type of the variables, the type of boxes. But you can put any values in those variables (any bit pattern). In Lisp, all the boxes, all the variables can hold any value, each value having some types. (a whole lattice of types in general).
1:17:22
pjb
For example, 42 is of type (integer 42 42), fixnum, (integer 0), (integer -1 333), of type (satisfies evenp), (member 21 33 42), (eql 42), etc…
1:18:33
nij_
Oh.. I should rephrase "I wonder how *usual* (i.e. non-CL) types are implemented then.. can they be implemented by the users?"
1:18:34
pjb
Note also that in lattices, there are elements that are not comparables (sets that are not subset one of the other).
1:33:46
jcowan
More broadly considered, in statically typed languages, types are the types of expressions, not only variables.
1:34:35
Bike
lisp types are attached to values rather than expressions or variables, which is part of why they're different
1:43:35
pjb
Because with change-class, a given object may have several different direct classes, at different times.
1:48:30
aeth
But if you do things that are so dynamic that they might break things, that's on you... if someone CHECK-TYPEs and you get around that, well, you're probably now breaking the assumptions of the program.
4:28:56
beach
nij-: It is types in other languages that are strange and complicated, yet restricted. They must be so that types can be determined statically. And they don't even succeed very well. Determining the exact type of an expression is undecidable in general, so those languages do what they can to make it decidable.