libera/#commonlisp - IRC Chatlog

20:25:57 Josh_2 Combining spinneret with the progn method combination is great :D

20:30:56 Guest82 Hi, sorry for the incredibly late reply (I've had a crazy time in my life lately...) but: Josh_2 contrapunctus shka loke[m] etimmons and beach thank you so much for answering me! on the questions I asked on July 4th! :D Thanks for pointing out at the commercial uses of lisp for web apps and the help dealing with some issue. Cheers!

20:31:42 phoe Guest82: no worries, a ping value of three and half a week is still tolerable on IRC

20:36:17 Guest82 thanks :D

20:49:49 pl Maybe worth job change I'll have the time to write some libs for a very commercial lisp use XD

20:50:54 pl In a world where vendor-locked IDEs are accepted, SBCL doesn't look that unique ;-)

20:54:57 shka pl: that's cool

20:57:14 phantomics Guest82: what were those commercial uses? Interested to see...

20:59:32 phantomics since you're back, Guest82: what were those commercial uses? Interested to see...

22:05:58 phoe is there a portable way to get a type specifier that matches only something of type X and not its subtypes?

22:06:11 phoe something equivalent to EQ CLASS-OF if we were talking classes instead

22:06:40 phoe if BAR inherits from FOO, I'd like something that is (AND FOO (NOT BAR)), except obviously I cannot enumerate all subtypes in the NOT because new ones can be created at any time

22:07:19 _death satisfies

22:07:40 phoe I was worried that would be the answer

22:13:31 _death out of curiosity, why do you want to do that?

22:15:26 phoe deep-copying structures around

22:16:29 phoe and thinking what exactly I want to achieve

22:17:02 _death I see

22:19:43 Bike i don't understand what exactly this would mean except in relation to classes

22:20:18 phoe yes, I'm still thinking

22:31:31 pjb phoe: subtypes are usually subsets.

22:31:41 phoe yes, I was talking garbage, don't mind me

22:32:21 pjb the only case is when you can't insert a type between tyep type and NIL. eg (subtypep 'nil '(integer 42 42)) #| --> t ; t |#

22:32:44 pjb For classes, that would be meaningful indeed.

22:32:45 moon-child pjb: types are not sets. Your broader point applies however

22:32:49 pjb = direct-instances

22:33:02 pjb moon-child: more or less, yes.

22:43:39 _death what are types if not sets?

22:44:07 moon-child https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

22:45:11 _death seems like an equivocation

22:45:29 phoe I mean, that's a long article

22:45:32 phoe is there a tl;dr?

22:45:44 _death in Common Lisp, types are sets

22:46:24 moon-child actually, since in common lisp types can be defined according to arbitrary predicates

22:46:35 Bike yeah, common lisp types wouldn't work for curry howard so well. they define a naive set theory.

22:46:35 moon-child types are classes

22:46:46 moon-child :^)

22:46:48 phoe more like the other way around

22:46:57 phoe KEYWORD is not a class even though I wish it was

22:47:09 _death I guess you mean "class" in the set theory sense

22:47:12 moon-child phoe: I mean, lisp-level types are maths-level classes

22:47:13 Bike also, the standard literally defines types to be sets within the context of the language, just to make it clear

22:47:14 phoe oh!

22:47:14 moon-child _death: yeah

22:47:17 phoe welp

22:47:36 _death but they are sets (which are classes)

22:48:16 Bike yeah, naive set theory. so things like "barbers that shave only those who do not shave themselves" are sets

22:48:42 Bike (satisfies barber-who-shaves-only-those-who-do-not-shave-themselves-p)

22:50:13 _death you need to provide the definition of this predicate :)

22:50:15 phoe how would you even properly express that in a CL type system

22:51:37 _death types are not first class objects in Common Lisp

22:51:45 Bike (defun type-that-contains-itself-p (type-specifier) (typep type-specifier type-specifier)) (satisfies type-that-contains-itself-p)

22:51:58 Bike for the actual paradox throw some nots in there

22:52:32 Bike and then marvel as a math thing from a hundred and twenty years ago leads to the practical consequence of needing to restart your lisp

22:52:46 phoe :(

22:54:47 Bike e.g., (typep 'cons '(satisfies type-doesnt-contain-itself-p)) => T, (typep '(cons t) ...) => NIL, (typep '(satisfies type-doesnt-contain-itself-p) '(satisfies type-doesnt-contain-itself-p)) => hang

22:55:07 Bike or just a stack overflow i guess. forgot about those

22:55:28 aeth SATISFIES is cheating, though

22:55:35 aeth since you can just do (loop)

22:55:40 phoe typep should be able to return (VALUES NIL NIL)

22:55:45 moon-child Bike: yeah, lots of things are easy to express mathematically but not so much in code

22:55:50 Bike i'm not talking about how to hang the type system, i'm talking about how types are sets.

22:55:50 moon-child see also: y combinator, in eager languages

22:55:58 Bike it's easy to express in code! the result just sucks is all

22:56:41 aeth hmm, apparently SBCL doesn't like me using FLET with a satisfies type

22:56:50 Bike satisfies is literally unrestricted comprehension. the lisp type system is set theory pre-russell.

22:56:59 Bike satisfies only works with global function names.

22:57:13 aeth (defun loop* (x) (declare (ignore x)) (loop)) (typep 42 '(satisfies loop*))

22:57:20 _death Bike: well, wasn't Russell's solution to introduce multiple levels (meta)

22:57:32 phoe is there any strictly technological reason why it cannot accept function objects?

22:57:42 phoe like `(satisfies ,(lambda (x) (oddp x))

22:57:44 aeth for all I know, other implementations do

22:57:46 Bike wasn't levels quine? or was everyone doing that?

22:58:06 Bike an implementation accepting a function would be nonconforming, and i don't think any of them do

22:58:11 Bike i don't think there's a technological reason though.

22:58:13 phoe yes, I know

22:58:14 _death think everyone was doing that, but not in that context

22:58:23 phoe just a question for the Hypothetical Future Revision™

22:58:36 _death I especially liked Tarski :)

22:58:46 Bike well tarski is the coolest logician.

22:58:47 phoe since type specifiers can already be unreadable, adding a function object in there won't break anything

22:58:56 Bike or was, i guess he's dead probably.

23:00:46 _death so the thing is, types are not first class objects.. you can only refer to them via type specifiers

23:00:58 Bike more seriously i think any HFT of types would warrant some thought about what types are actually for. i thought about it once and came up with four uses pulling them in different directions, though i don't remember the fourth now

23:12:15 aeth four?

23:12:32 aeth I can think of only two: types-for-verification and types-for-performance-hints.

23:12:40 aeth verification as in precondition/postcondition

23:19:26 Bike types are a predication DSL, used to describe constraints to the compiler for optimization, and used to describe storage classes for arrays and structures and stuff.

0:19:15 Guest82 Hi phantomics just seeing your message now

0:19:21 Guest82 give me a sec to get the link

0:21:30 Guest82 Here: https://irclog.tymoon.eu/libera/%23commonlisp?around=1625415280#1625415280

0:27:33 phantomics Guest82: thanks

0:27:41 phantomics I've also built web servers with CL, mostly serving React apps

0:28:55 Guest82 oh, that's what I'm trying to do phantomics :)

0:29:10 Guest82 did you use ngnix at all or just lisp?

0:29:23 Guest82 what libraries do you use?

0:29:29 Guest82 qlot and utopian or caveman2?

0:29:35 Guest82 or just hunchenhoot?

0:32:00 Guest82 phantomics do you use mito or your own classes?

0:38:15 phantomics Just built my own classes, haven't used with a relational DB

0:41:01 Guest82 ok, thanks... I'm trying now. I hope I will learn lisp but also be successful making an app haha

0:41:47 phantomics What's your goal app?

1:41:00 pjb phoe: note that deftype is like defmacro. If you allow closures in satisfies, each time the type is expanded you get a different closure!

1:41:32 pjb phoe: AFAICS, this is the reason why we're restricted to functions (that have to be defined in the compilation environment too, most of the time, so eval-when).

1:44:13 pjb phoe: but granted, it makes it very difficult to define list-of (deftype list-of (element-type) `(satisfies ,(once-or-twice (eval `(defun ,(gensym) (object) (is-proper-list-of ,',element-type object)))))) etc…

1:44:39 pjb in the current spec, you need to define a toplevel function for each type of list-of lists.

1:46:40 pjb phoe: perhaps like this: (deftype list-of (element-type) (let ((predicate (lambda (object) (typep object element-type)))) `(satisfies ,(compile (gensym) predicate))))

1:47:00 pjb I mean: (deftype list-of (element-type) (let ((predicate (lambda (object) (is-proper-list-of object element-type)))) `(satisfies ,(compile (gensym) predicate))))

1:48:22 pjb Yes, that works, with eg. (defun is-proper-list-of (object element-type) (and (proper-list-p object) (every (lambda (element) (typep element element-type)) object)))

1:50:57 pjb But as I said, this generates a new closure and a new toplevel function for each occurences of (list-of foo) (list-of foo) (list-of foo) -> 3 equal closures, 3 toplevel functions. So you want to manage a cache, which has the misfortune of having to live across the compilation-environment and the runtime environment. ie. you need to rebuild the cache at load-time or execute…

1:51:55 pjb satisfies would have to do the same without necessarily knowing what keys to use for the cache, if it had to deal with closures itself. at least, when the user does it, he knows what he's doing…