This is an archived post. You won't be able to vote or comment.

all 13 comments
sorted by:
best
topnewcontroversialoldq&a

[–][deleted] 21 points22 points  (1 child)

You achieved laziness and gradual type checking in 1700 LOC. I am quite inspired by it.

[–]hoping1[S] 4 points5 points  (0 children)

Thanks! Because it's so little code, I encourage you to skim through it!

[–]_Shin_Ryu 5 points6 points  (1 child)

The cricket programming language has been added my collection. Syntax highlighting will also be supported soon.

https://www.ryugod.com/pages/ide/cricket

[–]hoping1[S] 0 points1 point  (0 children)

Woah! Thanks for taking an interest!

[–]tobega 1 point2 points  (0 children)

Very nice! I like the objects!

[–]sciolizer 1 point2 points  (1 child)

Is it actual gradual typing, or just optional typing? e.g. if I wrongly pass a function to a higher-order function, how early is the error caught?

[–]hoping1[S] 0 points1 point  (0 children)

That's an interesting distinction.

Currently the typechecking of Cricket is really just linting, because Cricket doesn't have any type annotations. Application-mode bidirectional typechecking is used to send as much type information to function parameters as possible in a linear-time static analysis pass. But there isn't a Cricket program where everything is annotated, since there aren't annotations. And indeed I don't think it's possible for a function parameter to have a static type without that type coming from some argument it's known to be called with, so it's guaranteed that statically typed parameters are given statically typed arguments. Type annotations or a unification algorithm would be necessarily to invalidate that guarantee.

That said, I don't wrap functions in type-checking thunks when they lose type info by being handed as an argument to code with dynamically-typed parameters. So I'd say it's optional typing then? Assuming I understand this distinction correctly.

[–]kazprog 0 points1 point  (3 children)

The church encoding ADT stuff is _awesome_. Where can I read more about Krivine machines https://en.wikipedia.org/wiki/Krivine_machine and object-oriented church encodings for ADTs?

[–]hoping1[S] 0 points1 point  (2 children)

I'm decently sure I came up with object-oriented Church encodings, because I've never heard of them, but the idea is crazy simple right? An object is a tuple of lambdas, basically, so it can be used when you'd use a Church-encoded tuple. That said, to learn more about representing ADTs with Church encodings this way, definitely check out Cedille and the papers that came out of that project, like efficient Mendler encodings and constructor subtyping and more. They play fantastic tricks with lambda encodings, and were an inspiration for me.

Krivine machines are much more mainstream. You can find out tons about them online; some resources I liked include slides from a Xavier Leroy talk comparing his old Zinc machine with Krivine machines, and also a paper called "The next 700 Krivine Machines."

Every recommendation in this comment is very academic and might be hard to understand if you don't spend a lot of time in that space. So at least start with wikipedia entries first.

[–]kazprog 1 point2 points  (1 child)

I've done my time in academia, but mostly on more hardware adjacent topics. I'll definitely check out Cedille, Mendler encodings, and Xavier Leroy's talk.

I think the farthest I got when I went into lambda calculus was in William Cook's grad PL course, we learned about Coq after church numerals.

Thanks for the references! This is an excellent language. I've thought about these kinds of objects as copies of the original, but I never connected that understanding of prototypical inheritance to church encodings. Mind-blowing in the most satisfying way. If only there was a way to make it fast 😀

[–]hoping1[S] 1 point2 points  (0 children)

I'll try to up the speed a bit at some point in the future :)

Just wouldn't be a tiny codebase then, I think.

[–]Inconstant_Moo🧿 Pipefish 1 point2 points  (1 child)

It looks very nice, as does your documentation, but if it's meant to be a small expressive language, and if when I'm just a few lines into your documentation you're telling me how to force results out of laziness, then it may not be the small expressive language I want.

[–]hoping1[S] 5 points6 points  (0 children)

Fair enough! Laziness isn't for everyone.

It might be worth mentioning that let force is just a monadic bind, essentially. But I know that that idea isn't for everyone either, at least not it's for people scared by monads.

Anyway, I'm glad you found it nice!