How do I determine the breakpoint of a functor?
In Haskell, I can define the endofunctor endpoint like so:
data Fix f = Fix (f (Fix f))
But in Agda it cannot:
data Fix (F : Id (Set → Set)) : Set where
fix : (unId F) (Fix F) → Fix F
because it says, "The fix is not strictly positive because it occurs in the argument of a bound variable in the type of the fix constructor in the Fix definition."
I tried using Coinduction.∞
from 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
does not work.
I found this document which defines polynomial functors Functor
and a function [_] : Functor → Set → Set
that 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 be, and it is not, since both have a Fix
bound variable as an argument F
.
Is it possible to define a common endpoint in Agda, and if so how?
EDIT: This has been noted as a possible duplicate of 14699334 , but the only answer there is related to the Agda tutorial (?), Which includes fixing the point of the type of a specific polynomial functor; I want to know if this can be defined more generally. Specifically, I want to define fixed points of types that may be structurally equal, but nominally unequal.
source to share
No one has answered this question yet
See similar questions:
or similar: