Email or username:

Password:

Forgot your password?
31 comments
Devine Lu Linvega

*throws hands in the air*

Guess I'll add yet another god damn type

Capital

@neauoire Doing a bit of pen and paper computing, and I this is probably going to be a very hard problem to solve.

In the most general case, you are asking "does this loop terminate" which can't be solved (halting problem).

It could be possible to define some limited subset of loops that are known to terminate. However, this would require defining "finite data types" in Uxn and enforcing strings/arrays always end and numbers don't under/overflow.

Devine Lu Linvega

@CapitalEx OOOoooh, I think you're right. I hadn't made the connection with the halting problem, but that's true, I guess a specific type is indeed the solution here.

Capital

@neauoire :: (oops broke that one reply by accident)

Interested in what ideas you explore within Tal's limits. FP languages have the advantage of a strong type system and pattern matching. If your type is finite and each step reduces the given inputs to their base cases, you can say confidently that "this loop terminates".

Idris does this, but it also means some finite functions can't be statically resolved and are marked as partial.

Devine Lu Linvega

@CapitalEx I'm an absolute beginner when it comes to building type systems, so this is all fresh to me.

I've been going through the handlful of papers and blog posts on types/concat languages. This morning @toxi gave me a bunch of very interesting links on the topic: merveilles.town/@toxi@mastodon

I'll keep reporting my findings, I've started a stub on the topic here: wiki.xxiivv.com/site/type_syst

Karsten Schmidt

@neauoire @CapitalEx I just re-watched Jon Purdy's talk and it seems even 6 years later the number of people _actively_ researching/experimenting in this field is still extremely small! But this also means you're automatically kind of at the forefront and I'm looking forward to see what you'll come up with...

I'm still somewhat ambivalent about how far down the rabbit hole with respect to types in a Forth-style lang one should go before starting to compromise other core aspects like overall simplicity and actual utility. It's the same balance I'm striving to find in my TypeScript work. I do like structural typing and finding it very useful in general, but there're also a number of cases where I just learned to stay away from spending days/weeks on defining/refining/maintaining super complicated type constructs for very little practical gain. Types and type systems can be total nerd snipes and (IMHO) sometimes just spending more time on validation (where needed), documentation and explanations/reasoning of design decisions is time better spent than wasting it on super elaborate types. Sometimes it's just swapping one type of footgun for another and YAGNI... :)

@neauoire @CapitalEx I just re-watched Jon Purdy's talk and it seems even 6 years later the number of people _actively_ researching/experimenting in this field is still extremely small! But this also means you're automatically kind of at the forefront and I'm looking forward to see what you'll come up with...

Devine Lu Linvega

@toxi @CapitalEx I promise I'll try to not get sucked in too deeply that I can never re-emerge. :moomin_hello:

Devine Lu Linvega

No! Wait, I'm just dumb, the type checker was right and I couldn't understand what it was trying to tell me.

Haha, wow, it's a weird feeling when you build a thing to reflect about a problem and it starts to see things that you don't :maru:

spooky blip 👻

@neauoire this is the kind of joy I find in languages like TypeScript and Rust when I explain to people that the biggest win is in it checking my work and *proving* I didn't make logic mistakes (insofar as the type system can do)

some day eventually, I want you to investigate (as a purely learning experiment) tagged unions and exhaustiveness checking. by far one of my most-used features in those two mentioned languages, such checks genuinely made me a better developer.

Devine Lu Linvega

@klardotsh I wrote a tiny bit of Rust and I encountered the branch permutation checker, which is very cool. I'll look into the tagged union checker, that's something I've never heard of before.

anni

@neauoire I get the same feeling from my type inferencer all the time: Why is it complaining at me about this code? Oh, yeah, that's one on me!

nf

@neauoire a central part of my debugging process in general is to build tools to cross-check my observations. The best case is when you get two different but complementary failures, clues!!

Devine Lu Linvega

I'm starting to get the hang of this now.

So, one bad-habit that I had when building my wiki(which I've managed to overcome in the projects I've made afterward) was to hard-crash on error, no matter the stack state, and this just won't fly with the type checker, I've got to keep the stack in balance during error handling.

Ricardo B�nffy

@neauoire what environment are you running your blog in? The UI seems Oberon-like, but the language looks like Forth.

spooky blip 👻

@neauoire yaaaayyyy this is a lo-fi flavour of the Result<T> concept :) it's analogous to an Option<T> for methods (words) that might return null. I (very subjectively) find having to handle things in a balanced way like this leads to more understandable code.

blog.logrocket.com/understandi

Devine Lu Linvega

@klardotsh did you ever come across anything about type-checking in regards to concatenative languages by any chance? The body of work on the topic, that I can find, is extremely thin.

spooky blip 👻

@neauoire your assessment is correct. I never found much useful. I was planning my way around doing things very DIY and kinda blue collar since there's almost no academic research or past art to refer to, especially for my plans with Gale (inference, etc)

Devine Lu Linvega

@klardotsh everything that I could find, I've collected here: wiki.xxiivv.com/site/type_syst

I'll improve as I go along.

418 I'm a Teapot

@neauoire @klardotsh looks like you are in the Maybe monad... and maybe bind is the concatenation you are looking for...

Devine Lu Linvega

@chainik @klardotsh monad? in point-free assembly? I'm having trouble understanding what that might look like. Do you have a link on monads in Joy or Factor?

Avi Bryant

@neauoire @chainik @klardotsh I can imagine a Maybe monad in joy looking something like

wordThatReturnsMaybe [doSomethingToResult] map

or

wordThatReturnsMaybe
[anotherWordThatReturnsMaybe] flatMap

418 I'm a Teapot

@neauoire @klardotsh i don't have a concrete suggestion because my head isn't in the details. abstractly, i recognise Maybe and if the rest of the computation was happening in the monad it would type check :)

⛧ esoterik ⛧

@neauoire i'm not sure how your type-checker works but the way i'd handle this would be to confirm that the stack at the !&loop corresponds to the initial stack entering &loop. if that is true then you know it's preserving the shape and can just focus on the ?&exit condition

Devine Lu Linvega

@d6 that's how I do it at the moment, it's not throwing an error for the /l scope, it would if the entry and exit was unbalanced, but it's the scmp scope that throws an error since this routine doesn't have an obvious exit.

Here's a simpler version of that sort of routine which doesn't trigger an error.

⛧ esoterik ⛧

@neauoire i guess the checker doesn't know that ?&exit is a possible exit? i would have assumed that it follows both paths and then attempts to unify them later.

charlie

@neauoire wait but why would you want to trigger an error here, the code seems fine?

Devine Lu Linvega

@bellinitte the thing is that I don't want to trigger an error there, but the issue here is that the scmp routine promises to make an extra byte, and I don't know how to verify that this byte will be created until it reaches !&l.

I know it makes sense when you read the code, but I can't figure how who you find it programmatically.

Go Up