coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mu combinator

From: "John Wiegley" <johnw AT newartisans.com>
To: Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>
Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>, Igor Zhirkov <igorjirkov AT gmail.com>
Subject: Re: [Coq-Club] Mu combinator
Date: Wed, 30 Mar 2016 09:32:56 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f179.google.com
Ironport-phdr: 9a23:WlEUghcPfkXCp/Oa3cp1dM7HlGMj4u6mDksu8pMizoh2WeGdxc+6YB7h7PlgxGXEQZ/co6odzbGG4+a6CSdZuc/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uJM04R3GP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S4gUmIMiQZFBUDs6A33WJTwqCD6/r5B2C6AJtH7S/YdXSiv6aRqUhTooCEAKyI49m7Xg8k2hakdvRH39DJlxIuBKqOSNPw2QaLQctcXVCAJCsRWVypeKoWxcIIVE+saNOBD6YL6og1d/lOFGQCwCba3mXdzjXjs0Ph/irx5HA==
Organization: New Artisans LLC

>>>>> Thorsten Altenkirch
>>>>> <Thorsten.Altenkirch AT nottingham.ac.uk>
>>>>> writes:

> Why not just using the Church encoding:
> Definition Mu (f : Type -> Type) :=
> forall x, (f x -> x) -> x

Sure, you can use that too, you'll just need to know that it's a functor
"earlier" in some cases. I tend to Mendlerize by default in order to delay
requirements as late as possible, because then I can use plain composition to
manipulate the fixed point construction.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Mu combinator, Igor Zhirkov, 03/30/2016
- Re: [Coq-Club] Mu combinator, Thorsten Altenkirch, 03/30/2016
- Re: [Coq-Club] Mu combinator, John Wiegley, 03/30/2016
  - Re: [Coq-Club] Mu combinator, Thorsten Altenkirch, 03/30/2016
    - Re: [Coq-Club] Mu combinator, John Wiegley, 03/30/2016
- Re: [Coq-Club] Mu combinator, Gregory Malecha, 03/31/2016