How to disable typechecker in REPL

How can I skip typing in REPL (utop or stock ocaml) ? Ironic, isn’t ?

( Why on earth do I want that ? Because maybe I want to write Church numerals found in a lambda calculus course’s exercises which historically and academically comes first while learning ML )

Imagine what OCaml sternly replied when I fed it pred n ! The thing almost segfaulted in the cycle of a clock.

If not, is utop 's design allowing such feature ?

If still not, I’ll type the expressions myself some later time, please don’t spoil my learning, you erudite experts ! Just focus on the somewhat doomed question :hugs:

2 Likes

Hi @milvi,

This is not possible, unfortunately, as the translation from the source language to the underlying lambda calculus depends on the typing information.

On the other hand, you may be interested by https://github.com/stedolan/malfunction.

Cheers,
Nicolas

1 Like

Alternatively, you can try ocaml -rectypes and just ignore the types that are printed: in this mode, every term of the pure lambda calculus is typable, so you can play with Church numerals, combinators and so on.

4 Likes

:scream: what is thiiiiis ! looks really cool, though. You just cut a head of my Hydra of knowledge. Thanks. Now it has 7 more heads. Also I knew a degenerate OCaml turned Lisp would join the party.

Still, let’s call the 4 contributors of malfunction black camls, haha

From my point of view, this is so cool that ocaml becomes transparent to every term of lambda calculus by typing happily ever after in this typing space. I really wanted to be able to write everything in OCaml. You granted my wish in a “manual” way, thanks to the on/off switch right behind the box !

Seriously, who would have noticed on unpacking ! Easter egg :egg: :rooster:( I bet Coq has a basket of them too ).