6

In Haskell i can define an endofunctor fixpoint so:

data Fix f = Fix (f (Fix f))

But in Agda can't:

data Fix (F : Id (Set → Set)) : Set where
    fix : (unId F) (Fix F) → Fix F

as it says "Fix is not strictly positive, because it occurs in an argument to a bound variable in the type of the constructor fix in the definition of Fix."

I tried using Coinduction.∞ from the stdlib, in vain:

data Fix (F : Set → Set) : Set where
    fix : ∞ (F (Fix F)) → Fix F

or

data Fix (F : Set → Set) : Set where
    fix : F (∞ (Fix F)) → Fix F

neither works.

I found this doc which defines polynomial functors Functor and a function [_] : Functor → Set → Set which works:

data Functor : Set₁ where
    Id : Functor
    Const : Set → Functor
    _⊕_ : Functor → Functor → Functor
    _⊗_ : Functor → Functor → Functor

[_] : Functor → Set → Set
[ Id ] B = B
[ Const C ] _ = C
[ F ⊕ G ] B = [ F ] B ⊎ [ G ] B
[ F ⊗ G ] B = [ F ] B × [ G ] B

data Fix (F : Functor) : Set where
    fix : [ F ] (Fix F) → Fix F

but i'm not sure why that would and this wouldn't, as both have Fix as an argument to the bound variable F.

Can one define a general endofunctor fixpoint in Agda, and if so, how?

EDIT: This was marked as a possible duplicate of 14699334, but the only answer there links to an (the?) Agda tutorial which includes fixpoints of a specific polynomial functor type; i want to know whether one can define this more generally. In particular, i want to define fixpoints of types which may be structurally equal but are nominally inequal.

Community
  • 1
  • 1
M Farkas-Dyck
  • 646
  • 4
  • 14
  • 3
    Possible duplicate of [Recursion Schemes in Agda](http://stackoverflow.com/questions/14699334/recursion-schemes-in-agda) – Cactus Mar 29 '17 at 03:19
  • Are you sure that the Haskell data Fix is not just the Y-combinator? Could the Agda data Fix also be defined as a Y-combinator? I don't know Agda. It seems all functions are endo because they operate on themselves determined by type. Do you want a total function to handle any type? I just configure my functions to any type within reason. You can calculate with ['a'..'z'] but the calculation is mostly repetitious or boring unless maybe something in group theory. I know this is old and you've moved on but there were no comments even. – fp_mora Aug 01 '21 at 00:19

0 Answers0