The description is missing semantics, and the skeleton code only very briefly implicitly describes some semantics. Semantics for some functions can be extracted from the sample tests. This is however assuming too much on the part of the reader. Please add at least some semantic comments to functions plus, pred, and mult.

The most interesting part was at the very start, defining the term D and then figuring out how to use it to do Lambda Calculus. Once that was solved, the rest was pretty much the same as any other LC kata.

Still very interesting, I guess I was hoping for more "untyped" black magic.

Maybe you could use unsafeCoerce in Unsafe.Coerce.

Apparently Voile does not feel such explanation is necessary or he would have responded by now.

Also, this comment is not spoilered, so if people have trouble, they can read it.

Closing.

Haskell version GHC 8.8.4 has optimisation enabled by default. This clashes with the recursive type in this Kata and has to be disabled.

Hence {-# Options_GHC -O0 #-}

It turns out this can be implemented more elegantly in Ocaml (or "tagless-ly"), since Ocaml supports -rectypes command line option, which allow us to define types like type t=t->t. However, this is not enabled by default. Let me know if there's way to enable this...

Added, thanks!

Should add test case for pred, its much harder than succ/mult. Heres the one I used:

it "pred (x+1) = x" $ do 
        property $ \(NonNegative x) ->
          let x' = fromPeano (from $ x+1) :: D
          in showPeano (toPeano (pred `app` x')) == x

The signature showPeano :: D -> Int is a little clunky, since when you call it, you already know that you have a Nat; thus, I think that showPeano :: Nat -> Int might be a little cleaner. Personally, I also think it's a little strange that the warrior has to implement this at all, since it's sort of a digression from the rest of the problem.

In addition, I would write a couple helper functions for converting directly between Int and Church D (i.e. that combine showPeano, toPeano and from, fromPeano) to declutter the tests a bit.

I'm thinking about using type families to mimic the fold/unfold of recursive types, with some type functions making the projection automatic (like in DTALC). Not sure if it will work, but I'll try it out when I got some time.

It will be great if someone translate this to OCaml or any strict language, because the y combinator will mysteriously broke.
That will be a great lesson for anyone writing Definitional Interpreter - they share MetaLanguage characteristic, even sometimes unintentionally.
HOAS is another great example of the Object Language sharing the same characteristic of the MetaLanguage.

Haskell is HM (at least without wrapping), and UTLC is untyped. If you try to translate this kata to use plain haskell errors will show up.
For one you cant type the Y Combinator because it is recursive-typed. You do recursive type in Haskell by wrapping.
Peano Arithmetic also need System-F to type, and Rank Polymorphism have to be done... By wrapping again.

A fork just shows a variant. Note I varied in the solution as well as in the tests. You can have a look at it, but it's absolutely up to you what, if anything, you do with it.

If the source text uses D, go with that.

Hi Johan, Thanks for the valuable feedback and suggestions for improvement! The idea actually comes from TaPL, which you may preveiw here, starting at page p. 260. Pierce noted that recursive types can encode the whole untyped lambda calculus, which inspires me with the idea that "haskell is the most untyped typed language". Here D is chosen probably to mean "domain" (as in footnotes it says that "D's definition is precisely the universal domains used in semantic models of the pure lambda calculus").

What is also worth noting here is that Haskell can't directly encode recursive types without type tags (say the type "\m.int->m", which denotes a term that can accept infinite many integer parameters), and that's why we do a lot of wrappings and unwrappings. In fact, in Pierce representation, there are not type tags and app and lam are both of type D. Also, the use of explicit type tags here actually makes the problem looks easier, probably too easier--as there is only one way to write down the code. But in the original presentation with all terms being of type D, it's very surprising to see what we can do with recursive types. It would thus be interesting to see if we can get rid of the type tags and come up with a way to encode "tagless recursive types", maybe using universal types?

Finally, your suggestions all make sense to me, and I'll update the problem soon. By the way, since I'm new here, what does a fork mean? Is it something like git's fork-commit-pull-request pipeline, or it just shows a variant of the solution?