vintage screwlisp accountMay 6, 2025

Interview postponed / let's just talk about #types and #typing today's show on @dougmerritt and @vnikolov 's suggestion below.

(I'll speak a little bit to #Sandewall 's #SoftwareIndividuals #knowledgerepresentation

If anyone knows anything about #typetheory, that would be great.

https://anggtwu.net/math-b.html
https://www.hanselman.com/blog/stringly-typed-vs-strongly-typed
https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html
type links welcome

and #lisp

@shizamura possibly you can explain types of OWL to us instead of sleeping?

Eduardo Ochs - Academic Research - Categorical Semantics, Downcasing Types, Skeletons of Proofs, and a bit of Non-Standard Analysis

Show threadEduardo OchsMay 6, 2025

@screwtape Hey, I thought that today would be only a sound check, not the real interview... I am not prepared for the real interview! 😬😬😬

Can we postpone it? I will be super busy until may 20 - but I'll be have lots of time afterwards...

Show threadDougMerritt (log😅 = 💧log😄)

@eduardoochs @screwtape
Since it's now getting to be last-minute, to save screwtape's theme for today, it could just be about different things people mean by "types", laying the groundwork for whatever you have in mind later.

For instance, we could all roundly criticize "stringly typed"[1] 😉

[1] one of a zillion search results: https://www.hanselman.com/blog/stringly-typed-vs-strongly-typed

@vnikolov

Stringly Typed vs Strongly Typed

I used to call this technique 'type tunnelling' and noted its use in XML in ...

May 6, 2025 at 6:07pmWeb
Show threadVassil Nikolov | Васил НиколовMay 6, 2025

@dougmerritt @eduardoochs @screwtape

dougmerritt> we could all roundly criticize "stringly typed"

Yes, the latter is a far, far cry from (say) typed lambda calculus (among others).

By the way, note that lisp's eval does not take a string as its argument (unlike some other languages).

#Lisp
#StringlyTyped

Show threadvintage screwlisp accountMay 6, 2025

@eduardoochs
oh, sorry for the confusion! We can have a soundcheck before the show and /no/ interview.

@vnikolov @dougmerritt
types sound good. One thing I find confusing in Sandewall's work is that his typing was "you /must/ set an entity's type in its plist and are encouraged to use it []" (and 'new types' are entities of type thingtype)

Show threadvintage screwlisp accountMay 6, 2025

@vnikolov @dougmerritt
I guess you two remember I keep mentioning Goodwin 1981's Why Programming Environments Need Dynamic Types, in which Goodwin is basically suggesting lisp programmers to actively use DEFTYPE and TYPECASE (though at the time of writing, these were still congealing). Of course DEFCLASS and DEFSTRUCT implicitly DEFTYPE.

Goodwin, James W. "Why programming environments need dynamic data types." IEEE Transactions on Software Engineering 5 (1981): 451-457.

@eduardoochs

Show threadvintage screwlisp accountMay 6, 2025

@vnikolov @dougmerritt
in languages that handle PARSE-INTEGERable strings /such as #javascript (#Kitten)/ is the equivalence (sometimes) of "1" and 1 an example of defeasible inheritance?
In that
c = a - b
if c is 2 and a is 3, b might be a positive integer 1, or it might be a string "1" in js. #programming #types #defeasibleInheritance

@eduardoochs

Show threadDougMerritt (log😅 = 💧log😄)May 6, 2025

@screwtape @vnikolov @eduardoochs
That's something to argue about.

Some people like that kind of thing for rapid development.

Some people like the strongest possible typing in order to catch human error.

Show threadvintage screwlisp accountMay 6, 2025
@dougmerritt
The thing is that by arguing that you should be using DEFTYPE at runtime, isn't Goodwin arguing /for/ the strongest possible typing (Goodwin's enemy is using arrays as a sort of grab-bag I-don't-know-what-will-go-here type)
@vnikolov @eduardoochs
Show threadDougMerritt (log😅 = 💧log😄)May 6, 2025
@screwtape @vnikolov @eduardoochs
Strong typing comes in both static and dynamic flavors, although some people use more ambiguous terminology.
Show threadvintage screwlisp accountMay 6, 2025
@dougmerritt
the classic blog link above suggests strong means "that which makes me feel comfortable" and weak, "that which makes me feel uncomfortable"
@vnikolov @eduardoochs
Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 6, 2025

@screwtape @dougmerritt @vnikolov @eduardoochs That's the response of strong-typing fans, whatever they mean by that. If you're more a hippie dynamic coder:

Strong Typing: Like a cop sitting on my desk.
Weak Typing: Loose, easy, and groovy, man.

Show threadvintage screwlisp accountMay 6, 2025
@mdhughes
I want to link this to remembering fear and loathing yesterday. By the way, I was going to point out that fear and loathing on the campaign trail, (inb4 I get the 1972 election wrong) - Hunter had a very lawyer-esque companion with him on that campaign train that left without him - but /with/ the other guy who stood on the off-limits traintrack where staff couldn't get him and ruined the guy's campaign with heckling at the next speech.
@dougmerritt @vnikolov @eduardoochs
Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 6, 2025
@screwtape @dougmerritt @vnikolov @eduardoochs I keep meaning to read The Boys on the Bus, which I have but have barely read past Hunter's intro, and flipped thru the photos.
Show threadvintage screwlisp accountMay 6, 2025
@mdhughes
It's the second piece in the Kingdom of Fear collection I think. Oops, other thing.
@dougmerritt @vnikolov @eduardoochs
Show threadVassil Nikolov | Васил НиколовMay 6, 2025

@screwtape @dougmerritt @eduardoochs

What really matters is the amount of work to _fix_ or _change_ a program.
If you are so lucky to always write new programs that someone else fixes later and that never change, you can be comfortable with a lot of things...

Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 6, 2025

@screwtape @vnikolov @dougmerritt @eduardoochs I'm the classic "strong typing is for weak minds" guy, having done too much web dev, BASIC, REXX, shell scripts, etc. These let you trivially use strings as numbers, because user input is more important than "correctness" whatever that is.

If your focus is all careful math with units, then you want typing of some kind, but most of us code junky dialogues with users or real-world text files, so loose string handling is good.
#types #programming

Show threadvintage screwlisp accountMay 6, 2025

@mdhughes
I have this fantasy scenario though where I write a strongly typed program in the ACL2 lisp automatic theorem prover, and it automatically proves a bunch of useful lemmas, and then through curry-howard correspondence I somehow get those lemmas as a lisp package for outside lisp.

okay, it has never happened yet, but like, it could, right?

@vnikolov @dougmerritt @eduardoochs

Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 6, 2025

@screwtape @vnikolov @dougmerritt @eduardoochs Fantasy: Engine gives you awesome new information.

Reality: Fatal error: Type <T<Q:E>,D> unsatisfied at char 31,969.
#programming #types

Show threadVassil Nikolov | Васил НиколовMay 6, 2025

@screwtape @mdhughes @dougmerritt @eduardoochs

It could, but it is a lot of work to make it happen and there is too little demand to justify that work.

Show threadclewMay 6, 2025

But then Little Bobby Tables comes along…

Who has implemented “janky” as a type?

@mdhughes @screwtape @vnikolov @dougmerritt @eduardoochs

Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 6, 2025

@clew @screwtape @vnikolov @dougmerritt @eduardoochs The REXX data type is anything: string, integer, floating point with potentially bignum precision, or stem (associative array, key/value can be anything, by convention(!) .0 is length of an indexed array).

It's incredibly liberating if you just want to solve problems. It's scary to type-safety people.
#programming #types

Show threadvintage screwlisp accountMay 6, 2025
@mdhughes
Scary things:
cs-user> (typep (1+ most-positive-fixnum) 'integer)
t
cs-user> (typep (1+ most-positive-fixnum) 'fixnum)
nil
How often do numbers 281474976710656 or higher actually happen ;p
@clew @vnikolov @dougmerritt @eduardoochs
Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 6, 2025

@screwtape @clew @vnikolov @dougmerritt @eduardoochs

;; chez
;; dec is (fx- n 1)
> (dec (expt 2 59))
576460752303423487
> (dec (expt 2 60))
Exception in fx-: 1152921504606846976 is not a fixnum
Type (debug) to enter the debugger.
> (most-positive-fixnum)
1152921504606846975

Hrmn. If I avoid fixnum ops, I can let numeric tower pretend bignums are integers. I just need to make some ops that treat all strings as numbers, too.

Show threadVassil Nikolov | Васил НиколовMay 7, 2025

@screwtape @mdhughes @clew @dougmerritt @eduardoochs

screwtape> How often do numbers 281474976710656 or higher actually happen ;p

Depends on the domain.
The first example that comes to mind:
often enough if you calculate products of, say, 512-bit primes.

Show threadHunter JozwiakMay 7, 2025
@vnikolov @eduardoochs @dougmerritt @clew @mdhughes @screwtape They happen a lot in the idle games I play, for what that's worth.
Show threadvintage screwlisp accountMay 7, 2025
@sektor
yes in hindsight there is a countable infinity of them isn't there. Though my point @vnikolov
was mainly that with the tiny changes of 1+ chaing the number's type as a side effect, the program's behaviour radically changes (bignum + not fixnum +).
@mdhughes @clew @eduardoochs @dougmerritt
Show threadVassil Nikolov | Васил НиколовMay 7, 2025

@screwtape @sektor @mdhughes @clew @eduardoochs @dougmerritt

> there is a countable infinity of them

Pedantically, if you ignore that memory isn't unlimited.

> tiny changes of 1+ ... the program's behaviour radically changes (bignum + not fixnum +).

I see now.
That is a different point and yes, we ought to be aware of such things.
I can't improvise a proper discussion right now, but also compare to reading memory addresses past the end of a CPU cache line.

Show threadvintage screwlisp accountMay 7, 2025

@mdhughes
I finally got to the end of @smlckz ' article which I think captured some of our discussion here:

Static type checking shows that a program either is correct or else might be correct

and dynamic typing = testing shows that a bug either is present or else might be present.

@vnikolov @sektor @clew @eduardoochs @dougmerritt

Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 7, 2025

@screwtape @smlckz @vnikolov @sektor @clew @eduardoochs @dougmerritt
Static checking can only show that the program passes types down consistently, it says nothing about the logic or correctness of the program itself.
function addints(int x, int y) : int { return 3; }
is "consistent" and "type-safe", it returns an integer. But it's not "correct" for anything except addints(1,2).

Unit tests will quickly expose that addints is incorrect, even if you remove all the types.
#programming #types

Show threadvintage screwlisp accountMay 7, 2025

Unrelatedly and apropos nothing at all I mentioned satisfies before.

cs-user> (defun all-odd-p (sequence)
(notany 'evenp sequence))
all-odd-p
cs-user> (deftype very-odd-sequence () `(and sequence (satisfies all-odd-p)))
very-odd-sequence
cs-user> (typep #(1 3 5) 'very-odd-sequence)
t
cs-user> (typep #(1 3 5 2) 'very-odd-sequence)
nil

and I guess typecase - dynamic typing stuff. Idk (the very-odd-sequence foo)

@mdhughes @smlckz @vnikolov @sektor @clew @eduardoochs @dougmerritt

Show threadvintage screwlisp accountMay 7, 2025

@mdhughes
Sorry I had a misplaced reply. Another of the author's 8 points (surely you have to read the whole article to get the reward segment yourself, and not just skip directly to the bottom of the page) is

1. For what interesting properties of programs can we build static type systems?

So I guess the key thing about types is that they have to be syncronised to some kind of actual meaning.
@smlckz @vnikolov @sektor @clew @eduardoochs @dougmerritt

Show threadVassil Nikolov | Васил НиколовMay 7, 2025

@mdhughes @screwtape @smlckz @sektor @clew @eduardoochs @dougmerritt

The point is not that static type checking is omnipotent: it isn't, of course.
The point is that it catches _very many_ mistakes that programmers are _prone_ to make.
I say again: mistakes that are _often_ made, not all that can be made _in principle_.

> function addints(int x, int y) : int { return 3; }

This is too trivial.
Warning: variable declared but never used.

#StaticChecks
#StaticTypeChecks
#StaticTyping

Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 7, 2025

@vnikolov @screwtape @smlckz @sektor @clew @eduardoochs @dougmerritt
Anecdotal, but I almost never make the kinds of errors that type checking can find. I did make one a few weeks ago! I was very surprised, I'd passed an entirely wrong kind of object to a function. Once a year error. YMMV.

And yes, intentionally trivial example is trivial. Add
log("addints", x, y)
and now the type checker is a blind idiot again. You cannot make types enforce logic!

Show threadDougMerritt (log😅 = 💧log😄)May 7, 2025

@mdhughes
" You cannot make types enforce logic!"

Well hold on there, not so fast. You can in fact put *ALL* logic into a type system.

So you have to give a context for what you're talking about.

I agree that what you said is true of the most commonly used programming languages.

@vnikolov @screwtape @smlckz @sektor @clew @eduardoochs

Show threadDigital Mark λ ☕️ 🌮 🚀 🌗May 7, 2025

@dougmerritt @vnikolov @screwtape @smlckz @sektor @clew @eduardoochs Kurt Gödel disagrees. The Halting Problem disagrees.

Programming languages are in a sense a "logic system", but they don't prove anything, just bash numbers around like a rock tumblr until you get some gravel out. Is it the gravel you wanted? They *cannot* know.

Even inductive tools like Prolog just apply rules you've given, they can't prove those rules are logically correct.

Show threadVassil Nikolov | Васил НиколовMay 7, 2025

@mdhughes @dougmerritt @screwtape @smlckz @sektor @clew @eduardoochs

mdhughes:
<">
Kurt Gödel disagrees. The Halting Problem disagrees.
</">

Raising the stakes...

<">
... in a sense a "logic system", but they don't prove anything, just bash numbers around like a rock tumblr until you get some gravel out. Is it the gravel you wanted? They *cannot* know.
</">

For the record, I do believe this is only a part of the picture; the other parts are very significant, but alas, I can't elaborate now.

Show threadVassil Nikolov | Васил НиколовMay 7, 2025

@screwtape @mdhughes @smlckz @sektor @clew @eduardoochs @dougmerritt

Or:
"Beware of using this algorithm.
I have only proved that it is correct, but I haven't tested it."
(Donald Knuth; possibly apocryphal)

Show threadArtyom BologovMay 7, 2025

@screwtape I'm thinking about unary program encoding lately, so this is too small of a number actually!

@mdhughes @eduardoochs @vnikolov @dougmerritt @clew

Show threadVassil Nikolov | Васил НиколовMay 6, 2025

@mdhughes @screwtape @dougmerritt @eduardoochs

I disagree.
Remember the old joke that cowboy taxi drivers stop at green lights?

Show threadVassil Nikolov | Васил НиколовMay 6, 2025

@screwtape @dougmerritt @eduardoochs

screwtape> in languages that handle PARSE-INTEGERable strings /such as #javascript (#Kitten)/ is the equivalence (sometimes) of "1" and 1 an example of defeasible inheritance?

I don't know what defeasible inheritance is, but in JavaScript way too often this is a pain.
People even get into the habit of always writing things like (+x) instead of x...
I think this has already been elaborated.

Show threadVassil Nikolov | Васил НиколовMay 6, 2025

@screwtape @dougmerritt @eduardoochs

In spite of its name, `deftype' doesn't define a new type.
It defines a new name for an existing type.

#CommonLisp