• 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...

  • 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?

  • Maybe it's more different than less hardcoding, of course.

  • I'm conflicted.

    I like Haskell. And I like Lambda Calculus, a lot ( which is why I could easily find implementations for pred and y; the rest I could write without Googling ). ( Peano numbers have every right to feel like second rank citizens here. I don't like them as much. )

    This implementation seems to be a lot of wrapping and unwrapping ( which I have tried to make explicit in my implementations of L and lam ) around native Haskell function application and hardcoded Peano numbers for variables, thereby losing the polymorphism of being able to pass (+ 1) and 0 to Church numbers and getting an Int back, or alternatively (: '0') and "" and getting a base 1 encoded String back.

    Beneath all that, it's just plain Lambda Calculus in Haskell, which has been done before ( without all the [un]wrapping and the hardcoded type for variables ).

    This is not a useless duplicate - defining D is fun ( why "D" though? "Term"? ), though I would have liked the flexibility of naming N something else ( i.e. Variable. define deref cf. app, and you can test without hardcoding ). Testing does depend on certain implementation details, and those should be explained in the description. Don't comment out data D either - it must be there, so just put Data Term = Variable { deref :: Nat } | undefined. It may not compile, but it shows you need to fill in something. The initial code may compile, but figuring out which undefined barfs is more or less impossible anyway.

    I'll try to do a fork with less hardcoding.

  • ahh yes! At first I was thinking about abstraction in my mind but later found it conflicts with standard libraries and so rename it to lam, which stands for lambda. I'll update the description soon!

  • Loading more items...