Skip to content

Restrict (co)recursive instances#67

Draft
sellout wants to merge 2 commits intomainfrom
enforce-strictness
Draft

Restrict (co)recursive instances#67
sellout wants to merge 2 commits intomainfrom
enforce-strictness

Conversation

@sellout
Copy link
Owner

@sellout sellout commented Apr 1, 2025

This uses a Strict type family to tag types and type constructors with their strictness, allowing instances to be constrained more precisely.

This mitigates the issue that using a non-strict functor with, say, Mu will result in potentially infinite structures, since any functor used with Mu must be Strict in order to be folded.

loose ends

Before this PR is complete, the yaya-unsafe:Yaya.Unsafe.Fold.Instances module will go away in favor of instances defined over a newtype Unsafe t that will live directly in yaya-unsafe:Yaya.Unsafe.Fold. E.g.,

instance (Projectable (->) t f) => Projectable (->) (Unsafe t) f where
  project (Unsafe t) = project t

instance Recursive (Unsafe (Nu f)) f where
  cata φ (Unsafe nu) = unsafeCata φ nu

Comment on lines +36 to +47
-- | This tags types (and type constructors) with whether or not they are
-- strict.
--
-- A type is only strict when all the following conditions hold:
-- - no referenced type is non-strict
-- - no non-phantom type parameter is applied to a non-strict type
-- - all unapplied type parameters are strict (or phantom)
--
-- __FIXME__: This needs a third case (so, @`Maybe` `Bool`@) to distinguish
-- “simple” types that can be used birecursively, because they have
-- no recursive structure.
type family Strict (t :: k) :: Bool
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the main new thing added, and this needs instances for many cases.

On the plus side, if an instance is missing, the type that’s missing an instance won’t work with anything, so they can be added as needed.

Comment on lines +201 to 202
class (IsStrict t, IsStrict f) => Recursive c t f | t -> f where
cata :: Algebra c f a -> t `c` a
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Strict goes through a few layers, and is used here (and in Corecursive) to ensure the involved types have the required strictness.

Comment on lines 78 to 80
-- | When the pattern functor is not `Strict`, `Fix` may be used corecursively.
instance (IsNotStrict (Fix f), Functor f) => Corecursive (->) (Fix f) f where
ana ψ = embed . fmap (ana ψ) . ψ
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is an interesting consequence – when the functor is non-strict, Fix can be used corecursively. However, the same can’t be done with Mu, because embed (and project) on Mu requires cata, which has the IsStrict (Mu f) constraint, which would conflict with the IsNotStrict (Mu f) constraint required by ana.

@sellout sellout force-pushed the enforce-strictness branch 4 times, most recently from 8831a2b to 4795b96 Compare April 2, 2025 06:34
@sellout sellout force-pushed the enforce-strictness branch 2 times, most recently from 0c23eef to cbb975c Compare April 15, 2025 14:30
@sellout sellout force-pushed the enforce-strictness branch 2 times, most recently from e770b73 to 6025a49 Compare January 27, 2026 01:04
This uses a `Strict` type family to tag types and type constructors with their
strictness, allowing instances to be constrained more precisely.

This mitigates the issue that using a non-strict functor with, say, `Mu` will
result in potentially infinite structures, since any functor used with `Mu` must
be `Strict` in order to be folded.
@sellout sellout force-pushed the enforce-strictness branch from 6025a49 to ef98f43 Compare January 27, 2026 14:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant