leftaroundabout / constrained-categories Goto Github PK

When I first wrote the hierarchy, I didn't take good care to pick names that match the underlying mathematical terms. Thus, for example, Cartesian describes a symmetric monoidal category. Morphism doesn't have any more to do with morphisms than any of the other classes.

This keeps bugging me again and again. I will rename the classes some time later this year (hopefully).

Anybody who wants to chime in on what particular names to choose, feel free. I do still want to retain almost-compatibility with base:Control.Arrow, but it's perhaps not that important.

Could you explain the design behind Control.Category.Constrained.Reified — what use cases you have in mind and what salient alternatives are?

My context for asking is that

1. I am used to encountering statements like "Type t is isomorphic to the free f over some type constructor g", where such statements undergird useful constructions for working with DSLs defined by some g — free (co)monads over a polynomial functor, etc.
2. I understand GHC's type inference about things as complex as the types introduced in this package is not quite as powerful as one might like, and that means there are some things one might be able to express but which might be awkward or difficult to use.
3. The constraints on the constructors of all the reified free types in Control.Category.Constrained.Reified presuppose that the category type you're constructing a free x structure over already have an x instance: e.g. the Object constraints on CategoryId and CategoryCompo entail that you can only construct an ReCategory k value for a k that already has a Category instance.

Unless I'm missing something, item 3 means that the types in the Reified module may still be useful for constructing "unevaluated" DSL fragments that can then be interpreted in different ways provided you do all the work to define an x instance in the first place, but there's no support for the class of use cases in item 1: there's no support for freely lifting a primitive type k into a Category (or a Cartesian one, etc.). What's the story as to why?

I'd guess the answer has to do with object + morphism constraints and some combination of type safety + ergonomics, but I'd appreciate having some of that spelled out.

I was wondering if you could comment on this design decision?

I noticed Conal Elliot went with type Object k :: Type -> Constraint in concat

And this library chooses type Object k a :: Constraint (line #).

I'm just curious what trade-offs you've noticed/anticipated?

EDIT: interestingly, Conal has an experiment with the same Object you use in this lib.

I'm personally interested in reviving this space of a categorical prelude, and just curious what the current options are, and where I should place my efforts.

I was wondering if you could comment on this too, the Readme suggests that subhask will succeed constrained-categories? subhask's last commit was 6 years ago and seems rather dead, and if it is indeed dead, what were some of the benefits you saw in that library over constrained-categories?

How would you suggest defining foldMap for a type-aligned list ("value of the free category over some p a b"), given the definitions below?

{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}

import Prelude hiding (id, (.), map, foldMap)
import Control.Category.Constrained
  (Category (Object, id, (.)))

data FreePath p a b where
  Nil   ∷ FreePath p a a
  (:<)  ∷ b `p` c → FreePath p a b → FreePath p a c
  (:<:) ∷ FreePath p b c → FreePath p a b → FreePath p a c

instance Category (FreePath p) where
  id  = Nil
  (.) = (:<:)

map ∷ (∀ x y. x `p` y → x `q` y) → FreePath p a b → FreePath q a b
map _ Nil        = Nil
map f (m :<  p ) = f m :< map f p
map f (p :<: p') = map f p :<: map f p'

-- How do I define foldMap? What constraints are necessary/sufficient for that?
-- Is [this discussion](https://github.com/leftaroundabout/constrained-categories/issues/6) relevant?

foldMap ∷ ∀ p q a c. (Category q, Object q a, Object q c)
        ⇒ (∀ x y. x `p` y → x `q` y) → FreePath p a c → a `q` c
foldMap _ Nil        = id
foldMap φ (m :<  p ) = φ m . foldMap φ p
foldMap φ (p :<: p') = foldMap φ p . foldMap φ p'


foldMap' ∷ ∀ p q a b c. (Category q, Object q a, Object q b, Object q c)
         ⇒ (∀ x y. x `p` y → x `q` y) → FreePath p a c → a `q` c
foldMap' _ Nil                                              = id
foldMap' φ ((m ∷ b `p` c) :< (p ∷ FreePath p a b))          = φ m . foldMap' φ p
foldMap' φ ((p ∷ FreePath p b c) :<: (p' ∷ FreePath p a b)) = foldMap' φ p . foldMap φ p'

I think I understand the basic issue as the typechecker needing some reason to believe that every single intermediate type y in a sequence (p y z) :< (p x y) needs to satisfy the constraint Object q.

However, I'm not sure what some reasonable conditions are under which that would hold or how to express them:

• When Object q is the trivial or vacuous constraint, this should be definable.
• If p is already a Category instance and p and q are such that Object p z always entails that Object q z holds, this should be definable.

Does the embedding constructor (:<) of FreePath need to be constrained? If so, how?

EDIT: Corrected the RHSs of the :<: case of foldMap, foldMap'.

Thanks for the help on Stackoverflow today! I've really been enjoying getting to know your library, and in conjunction, learning tradeoffs between your approach and that of Conal Elliot in concat, namely, his objects look more like type Object k :: * -> Constraint. (If you know of any literature, discussion group threads etc on the tradeoffs between the 2 approaches, please let me know!)

Anyway, I wanted to share an extension to Agents I've been playing around with that makes it act a little more like proc syntax, namely, allowing for tuples of GenericAgents. It's messy, I could probably simplify it, but, it works!:

type O4 p a b c d = (Object p a, Object p b, Object p c, Object p d)
type O6 p a b c d e f = (Object p a, Object p b, Object p c, Object p d, Object p e, Object p f)

-- | Interpret tuples of 'GenericAgent' as just a 'GenericAgent'.
class AgentParam p q b where
  type AgentParamC p q b :: Constraint
  type AgentParamOutTy p q b
  agentParam :: AgentParamC p q b => b -> GenericAgent p q (AgentParamOutTy p q b)

instance AgentParam p q (GenericAgent p q a1, GenericAgent p q a2) where
  type AgentParamC p q (GenericAgent p q a1, GenericAgent p q a2)
    = (O4 p q a1 a2 (a1, a2), PairObjects p a1 a2, PreArrow p)
  type AgentParamOutTy p q (GenericAgent p q a1, GenericAgent p q a2)
    = (a1, a2)
  agentParam (x, y) = GenericAgent (runGenericAgent x &&& runGenericAgent y)

instance AgentParam p q (GenericAgent p q a1, GenericAgent p q a2, GenericAgent p q a3) where
  type AgentParamC p q (GenericAgent p q a1, GenericAgent p q a2, GenericAgent p q a3) =
    (O6 p q a1 a2 a3 (a2, a3) (a1, (a2, a3)), PairObjects p a2 a3, PairObjects p a1 (a2, a3), PreArrow p)
  type AgentParamOutTy p q (GenericAgent p q a1, GenericAgent p q a2, GenericAgent p q a3) =
    (a1, (a2, a3))
  agentParam (x, y, z) = GenericAgent (runGenericAgent x &&& runGenericAgent y &&& runGenericAgent z)

-- | Arrow-like interface
f $-< x = f $~ agentParam x   -- hm... this is tough to type

This allows syntax like:

let       out = SomeArr <<< WowArr $-< (x, y)

     vs

proc ...  out <- SomeArr <<< WowArr -< (x, y)

This allows tupling on the input side. Then on the output side, it'd be nice if we could pattern match, like proc syntax can, so, I'm wondering if I could do something with PatternSynonyms there too, but, haven't gotten around to it yet.

Anyway, just wanted to let you know, and if this is interesting or deserves pursuit, lmk, I'd be happy to contribute a PR!