Support type predicates

[porcuquine]

There is currently no way to check the type of a Lurk expression. Although this can frequently be worked around, this needs to be possible in general. The most obvious approaches have some problems.

For example, consider:

• Explicit type names, like Common Lisp's typep: (typep 123 'number) => t This will be expensive because of the required indirection through the symbolic type name. Of course there are benefits to the rich types such an approach makes possible, but this is very expensive for the minimal primitive type discrimination required.
• Explicit access to type tags, like (type-eq 123 4) This is way too concrete. We don't want to expose the literal representation of Lurk expression tags in this way.

Fortunately, there is a good solution which is cheap and — although a bit quirky — perfectly understandable.

Specifically, we can support a prototype-based type predicate that requires presenting a literal of the intended type for comparison. The obvious name for this predicate is same-type?, and some examples should make the idea clear.

> (let ((x 123)
    (same-type? 0 123))
t
> (let ((x 123)
    (same-type? :x x))
nil
> (let ((x :asdf))
    (same-type? :x x))
t

This is very cheap to support, and is fact cheaper (in constraints) than either = (which requires type checking) or eq, which requires two equality checks. same-type? requires only a single equality check on the tags of its arguments; and ignores their values. This makes it a beautiful and obvious operation to support in terms of Lurk's circuit-centric economic aesthetic.

[arthurpaulino]

Given that we have eq, would type-eq be a more consistent name? E.g. (type-eq 0 0)

[porcuquine]

Yeah, maybe so.

[arthurpaulino]

What kind of bugs me with this approach is that type-equality doesn't entail a particularly interesting semantic for two arbitrary inputs. So what's likely to happen with real Lurk code is that people will use it with a dummy value (e.g. 0, 'a' or "") in the second argument.

The issue is not simply aesthetic. With two arguments, it becomes a binop, forcing the machine to spend an extra iteration everytime to evaluate those trivial values.

The other approach is having specific operators like num?, str? etc. But it's not perfect either, as more operators increase overall circuit size whereas the extra iteration from type-eq is amortized by higher reduction counts.

[porcuquine]

I would define it to the first argument is not evaluated and must be a literal.

[porcuquine]

Cost-wise this will make it a unop. You can create a unop continuation that captures the first tag, discards the value (or not) and then expects the evaluation on the second arg.

[porcuquine]

That was implicit in the description and examples above, but I should have mentioned it explicitly.

[arthurpaulino]

Then it enters this territory of semantic ambiguity. For example, in my mind it would be more natural for the second argument not to be evaluated because that's where literals usually go. E.g. (+ x 1).

These design decisions that involve asymmetries behind the curtains often put the users in an "which one was it?" state

[porcuquine]

Not really. You can think of it ad currying/partial-evaluation. Your example is good, since CL has a function 1+.

[porcuquine]

In any case, there would be no ambiguity. The behavior would be defined.

[arthurpaulino]

Defined/documented behavior doesn't completely mitigate the issue I am pointing at. If the first argument is the one that wouldn't be evaluated, then here's another idea to the pool: same-type-of. Then (same-type-of 0 x) would be very natural to even speak out loud. It's actually a slight variation of your first proposal.

[porcuquine]

Oh, if you’re just wordsmithing your name suggestion then I agree. That was the original same-type? idea. Now that we’ve gone around the block, I think same-type-as might be the best.

[arthurpaulino]

In the beginning I thought that we would evaluate both arguments (hence the parallel I made with eq). But after you mentioned that only one of them would be evaluated, I went with the idea.

Ah, question... what if the user wants to do logic checking if a variable is bound to a function?

[porcuquine]

In this theory, we would need to provide a literal syntax for functions. If we did, that would usually be preferable (cheaper) for users, when they don't require closures. (The reader should not track lexical environments, which are related to evaluation — so couldn't create proper closures.) So it should probably be syntactically close to a normal lambda.

A simple and general-purpose answer might be to support CL's #. syntax directly (or something equivalent — but I'd argue for matching it). This is a reader macro that performs read-time evaluation. For example, #.(+ 1 1) would be read as 2.

Note that this behaves as expected in CL:

(funcall (let ((x 1)) #.(lambda () x)))
; in: LAMBDA ()
;     (LAMBDA () X)
; 
; caught WARNING:
;   undefined variable: COMMON-LISP-USER::X
; 
; compilation unit finished
;   Undefined variable:
;     X
;   caught 1 WARNING condition
; in:
;      FUNCALL (LET ((X 1))
;            #<FUNCTION (LAMBDA ()) {7006B803CB}>)
;     (X 1)
; 

But

CL-USER> (funcall #.(lambda () 3))
3

So in your case, you could say, e.g. (same-type-as #.(lambda ()) x).

[porcuquine]

I have to say that same-type-as gets the meaning right but is kind of unwieldy.

I'd probably prefer something like type=, where the user is simply required to understand the semantics (which is unavoidable regardless).

[arthurpaulino]

Why was the issue closed?

[porcuquine]

Just bad GH ux/operator error.