Constraints and defining `foldMap` for a free category?

emeinhardt commented 1 year ago

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'.

leftaroundabout commented 1 year ago

Nice question! But first: the b in the signature of foldMap' isn't supposed to be there, right?

leftaroundabout commented 1 year ago

Second: this isn't really the free category, is it? Shouldn't we normalize any composition to the form f:<(g:<(h:<(...)))?

Though I suppose that doesn't have any bearing on the question here.

...Well, maybe it does actually matter. At any rate, surely it should be

foldMap φ (p :<: p') = foldMap φ p . foldMap φ p'

not foldMap φ p :<: foldMap φ p', right?

leftaroundabout commented 1 year ago

To get to the actual crux: adding constraints to :< could make sense, but it wouldn't be enough for foldMap to typecheck. Basically, you'd need its signature to be

foldMap ∷ ∀ p q a c. (Category q, Object q a, Object q c)
        ⇒ (∀ x y r . (Object p x, Object p y) ⇒ x `p` y
                → ((Object q x, Object q y) ⇒ x `q` y → r)
                → r)
                → FreePath p a c → a `q` c

That could probably be made to work, but it's mighty awkward. We could, I suppose, introduce a wrapper for this kind of "constraint-propagating mapping", either

data ConstraintPropagating p q = ...

or

type CAT = Type → Type → Type
class ConstraintPropagating (m ∷ k) (p ∷ CAT) (q ∷ CAT) | m → p, m → q where
  proveTgtConstraint ∷ ∀ r x y . (Object p x, Object p y) ⇒ ((Object p x, Object p y) ⇒ r) → r
  morphMapping :: ∀ x y . (Object p x, Object p y) ⇒ p x y → q x y

But this still feels like clunky and missing the point of what we're really trying to do. Perhaps this should just be a Functor? After all, it feels a lot like we're really supposed to be talking about natural transformations.

emeinhardt commented 1 year ago

Minor clarifications

Nice question! But first: the b in the signature of foldMap' isn't supposed to be there, right?

It's there on purpose in a very weak sense ¯\(ツ)/¯. Both foldMap and foldMap' in my first post are incomplete and in-progress - neither typechecks as they are, and the b is a bit of type-level debris to placate GHC and reveal more informative error information. foldMap' is there because of my loose understanding of how constraints, instance resolution, and quantification interact; relative to foldMap, I thought ScopedTypeVariables might be helpful to GHC or to me in understanding GHC's errors, and that's the main difference between foldMap and foldMap'. I think it may be best to ignore foldMap'.

At any rate, surely it should be foldMap φ (p :<: p') = foldMap φ p . foldMap φ p' not foldMap φ p :<: foldMap φ p', right?

Yes - list constructors should be replaced with corresponding category operations. Thanks for catching that!

How should FreePath be defined?

Second: this isn't really the free category, is it? Shouldn't we normalize any composition to the form f:<(g:<(h:<(...)))?

I can see why that makes sense - it exposes the relevant type variables and should generalize to arbitrary length constructions. However, I'm not sure concretely what you had in mind:

just changing pattern matching as needed to reflect your suggestion
or something more than just that (setting aside the larger issue of constraint propagation).

Once I expand the pattern matching, it seems - as you put it with respect to constraint propagation - that the redundancy between :< and :<: makes things a bit clunky. Salient options for changing the definition of FreePath include

Removing the :<: constructor, because it can be derived from :< and fold{Map,r}.

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

Changing the embedding constructor so it does just that and nothing else: i.e. replacing :< with Emb ∷ p a b → FreePath p a b.
```
data FreePathEmb p a b where
Emb   ∷ a `p` b → FreePathEmb p a b
Nil   ∷ FreePathEmb p a a
(:<:) ∷ FreePathEmb p b c → FreePathEmb p a b → FreePathEmb p a c
```
Option 1 complicates the definition of a Category instance. Option 2 introduces some extra nesting noise in pattern matching; perhaps introducing a view pattern (pattern synonym?) could alleviate this a bit.

Your remarks in your most recent comment also suggest to me a third option:

Shifting to a circumfixing, ListZipper-like, profunctor-like construction:

data FreePathCirc p a b where
Emb   ∷ a `p` b → FreePathCirc p a b
Nil   ∷ FreePathCirc p a a
(:><) ∷ FreePathCirc p c d → FreePathCirc p a b → FreePathCirc p b c → FreePathCirc p a d 
-- NB argument order of `:><` mimics the convention that has emerged for the arguments 
-- of `dimap` modulo keeping the order of composition (dataflow direction) the same as (.)

Constraint propagation and a concise formulation of foldMap

On that note - profunctors (not their definition in most Haskell packages per se, where obligatory contamination by Hask is part of the price of their ergonomics) and your last comments about looking for a functor or something related to natural transformations - none of these FreePath definitions allow for the arguments of p to be constrained.

That's a simplification for now, but a defect in light of some of the use cases that motivate this package, no? Perhaps accounting for this may also point towards better formulations of foldMap - or leave them as the only options that will typecheck.

But this still feels like clunky and missing the point of what we're really trying to do. Perhaps this should just be a Functor? After all, it feels a lot like we're really supposed to be talking about natural transformations.

I will have to think more about this (and read enough about natural transformations to see exactly where the relevant types would line up), but my first thought is that some of the constructions in the vitrea package might be helpful: I'll play around with these in a cabal REPL, focusing on FreePathCirc.

emeinhardt commented 1 year ago

Poking around further in other parts of the constrained-categories repo and nlab got me to this functor-based definition that compiles:

{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import Prelude hiding
  (id, (.), Functor, fmap, Foldable, foldMap)
import Control.Category.Constrained
  (Category (Object, id, (.)))

infixr 9 ∘
(∘) ∷ (Category k, Object k a, Object k b, Object k c)
    ⇒ b `k` c → a `k` b → a `k` c
(∘) = (.)

data FreePath p a b where
  Emb ∷ (Category p, Object p a, Object p b) -- aka singleton
      ⇒ a `p` b → FreePath p a b
  Id  ∷ (a ~ b, Category p, Object p a, Object p b) -- aka []/mempty 
      ⇒ FreePath p a b
  Of  ∷ (Category p, Object p a, Object p b, Object p x) -- aka (++)/(<>)
      ⇒ FreePath p x b → FreePath p a x → FreePath p a b

class Object p a ⇒ Object' p a
instance Object p a ⇒ Object' p a

-- | @φ@ represents some functor's mapping of objects of @r@ to objects of @t@;
-- @α@ represents the same functor's mapping of morphisms of @r@ to morphisms of @t@.
foldMap ∷ ∀ φ r t a b. (Category r, Category t, Object r a, Object r b
                       , ∀ z. Object' r z ⇒ Object' t (φ z))
        ⇒ (∀ x y. (x `r` y) → (φ x `t` φ y))
        -- NB The three alternative type signatures below will also compile;
        -- I believe the next two below are equivalent to each other.
        -- ⇒  (∀ x y. ((Object r x, Object r y, Object t (φ x), Object t (φ y))
        --           ⇒ (x `r` y) → (φ x `t` φ y)))
        -- ⇒  (∀ x y. ((Object r x, Object r y) ⇒ (x `r` y)
        --             → ((Object t (φ x), Object t (φ y)) ⇒ (φ x `t` φ y))))
        -- ⇒ (∀ x y. (Object r x, Object r y, ∀ w. Object' r w ⇒ Object' t (φ w))
        --           ⇒ (x `r` y) → (φ x `t` φ y))
        → FreePath r a b → (φ a `t` φ b)
foldMap α (Emb p)    = α p
foldMap _  Id        = id
foldMap α (q `Of` p) = (foldMap α q) ∘ (foldMap α p)

Note that GADT constructor constraints and a

∀ z. Object' r z ⇒ Object' t (φ z)

constraint (enabled by what you mention at the end of this comment of yours) are crucial for allowing Object constraint information to propagate in a manner legible to the typechecker here. Is there a similarly concise alternative that doesn't require UndecidableSuperClasses?

What kind of functor typeclass were you thinking that would avoid the need for existential types? The analogue of the (four) type(s) for α I have above is given by:

{- | A functor @φ@ from @r@ to @t@
    1. should map every object @a@ of @r@ to an object @φ a@ of @t@.
    2. should map every morphism @a `r` b@ to a morphism @φ a `t` φ b@.

   #1 is taken care of in Haskell by the data constructors of @φ@; #2 is the job of the definition
   of @fmap@ in the @Functor@ instance for @φ@, and every definition for @fmap@ should ensure the
   following equalities hold:

   @
     fmap (g ∘ f) = fmap g ∘ fmap f
     fmap id = id
   @
-}
class (Category r, Category t) ⇒ Functor φ r t where
  fmap ∷ ∀ a b. (a `r` b) → (φ a `t` φ b)
  -- fmap ∷ ∀ a b. (Object r a, Object t (φ a), Object r b, Object t (φ b))
  --      ⇒ (a `r` b) → (φ a `t` φ b)
  -- fmap ∷ ∀ a b. ((Object r a, Object r b) ⇒ (a `r` b)
  --           → ((Object t (φ a), Object t (φ b)) ⇒ ((φ a) `t` (φ b))))
  -- fmap ∷ ∀ a b. (Object r a, Object r b, ∀ x. Object' r x ⇒ Object' t (φ x))
  --      ⇒ (a `r` b) → (φ a `t` φ b)

My few attempts at extending foldMap to natural transformations ('foldNat'?) have led to a headspinning amount of bookkeeping, so I think I'd like to explore the space of options for a functor-based foldMap first.

emeinhardt commented 1 year ago

Some lightly cleaned up definitions that support lifting a type that isn't already a category into the FreePath + some simple example code demonstrating that foldMap more than just typechecks:

Revised definitions

{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}

import Control.Category.Constrained
  (Category (Object, id, (.)))
import Data.Functor.Identity
import qualified Prelude as Pr
import Prelude hiding
  (id, (.), Functor, fmap, Foldable, foldMap)
import Data.Kind (Type, Constraint)

infixr 9 ∘
(∘) ∷ (Category m, Object m a, Object m b, Object m c)
    ⇒ b `m` c → a `m` b → a `m` c
(∘) = (.)

-- @p@ is expected but not required to be a category here: @φ@ corresponds to the constraint (if any)
-- on objects of the category.
data FreePath (p ∷ Type → Type → Type) (φ ∷ Type → Constraint) (a ∷ Type) (b ∷ Type) where
  Id  ∷ (φ a, φ b, a ~ b) ⇒                                       FreePath p φ a b
  Of  ∷ (φ a, φ b, φ x  ) ⇒ FreePath p φ x b → FreePath p φ a x → FreePath p φ a b
  Emb ∷ (φ a, φ b       ) ⇒ a `p` b                             → FreePath p φ a b

class    Object p a ⇒ Object' p a
instance Object p a ⇒ Object' p a

-- | If values of @FreePath p@ represent 'programs' over the primitives offered by @p@, this instance allows
-- for the definition of 'program transformations' ("endofuctors") via @foldMap@.
instance Category p ⇒ Category (FreePath p (Object' p)) where
  type Object (FreePath p (Object' p)) o = Object p o
  id  = Id
  (.) = Of

-- | @γ@ represents some functor's mapping of objects of @r@ to objects of @t@;
-- @α@ represents the same functor's mapping of morphisms of @r@ to morphisms of @t@.
-- Note that @r@ is expected but not required to be a Category with some object
-- constraint @φ@; i.e. if @r@ is a (constrained) Category instance, than it is
-- expected that @φ@ = @Object r@/that @φ x@ ≡ @Object r x@.
foldMap ∷ ∀ φ γ r t a b. (Category t, φ a, φ b, ∀ z. φ z ⇒ Object' t (γ z))
        ⇒ (∀ x y. (x `r` y) → (γ x `t` γ y))
        → FreePath r φ a b → (γ a `t` γ b)
foldMap α (Emb p)    = α p
foldMap _  Id        = id
foldMap α (q `Of` p) = (foldMap α q) ∘ (foldMap α p)

Some arithmetic++ primitives

-- | A variant on the common arithmetic++ toy/demo DSL, bashed into the shape of
-- unary functions.
-- This may be too simple to be the most useful demo/test case - *every* constructor either explicitly
-- requires the category constraint or it specifies a concrete type that has an explicitly given instance;
-- A more usefully interesting test case may be to define a more typical arithmetic expression DSL and then
-- define some (unary) morphisms.
data ArithFunc a b where
  Lit    ∷ (ArithPrim b) ⇒ b     → ArithFunc ()   b
  Inc    ∷                         ArithFunc Int  Int
  Dec    ∷                         ArithFunc Int  Int
  EqlTo  ∷ (ArithPrim a) ⇒ a     → ArithFunc a    Bool
  Ite    ∷ (ArithPrim b) ⇒ b → b → ArithFunc Bool b

deriving instance (Show (ArithFunc a b))

class (Show x, Eq x) ⇒ ArithPrim x
instance ArithPrim Int
instance ArithPrim Bool
instance ArithPrim ()

Some example expressions

Below are some example programs in the DSL defined by lifting ArithFunc primitives into the free category ('quiver'?) definable via FreePath:

type FreeArithFunc a b = FreePath ArithFunc ArithPrim a b

noOp ∷ ArithPrim a ⇒ FreeArithFunc a a
noOp = Id

one ∷ FreeArithFunc () Int
one = Emb $ Lit 1

two ∷ FreeArithFunc () Int
two = Emb $ Lit 2

sub1 ∷ FreeArithFunc Int Int
sub1 = Emb Dec

alsoOne ∷ FreeArithFunc () Int
alsoOne = sub1 `Of` two

alsoOneIsOne ∷ FreeArithFunc () Bool
alsoOneIsOne = Emb (EqlTo 1) `Of` alsoOne

boolToInt ∷ FreeArithFunc Bool Int
boolToInt = Emb (Ite 1 0)

alsoOneIsOne' ∷ FreeArithFunc () Int
alsoOneIsOne' = boolToInt `Of` alsoOneIsOne `Of` noOp

foldMap and friends

-- This would be the `fmap` definition for a functor instance relating `Identity`, `ArithFunc`, and `Hask`
evalCalc ∷ ∀ a b. ArithFunc a b → (Identity a → Identity b)
evalCalc (Lit b)   = Pr.fmap $ const b
evalCalc  Inc      = Pr.fmap $ (+ 1)
evalCalc  Dec      = Pr.fmap $ (subtract 1)
evalCalc (EqlTo a) = Pr.fmap $ (== a)
evalCalc (Ite t e) = Pr.fmap $ \test → if test then t else e

evalCalc_ ∷ ∀ a b. (ArithPrim a, ArithPrim b)
          ⇒ FreePath ArithFunc ArithPrim a b
          → (Identity a → Identity b)
evalCalc_ = foldMap evalCalc

unId ∷ (Identity a → Identity b) → (a → b)
unId f = runIdentity ∘ f ∘ Identity

-- More convenient to work with for checking that you can actually perform calculations
evalCalc' ∷ ∀ a b. (ArithPrim a, ArithPrim b)
          ⇒ FreePath ArithFunc ArithPrim a b
          → (a → b)
evalCalc' f = unId $ evalCalc_ f

As far as foldNat goes, I'm looking at whether a cons-based representation for FreePath is any easier for me to work through than the current concatenation-like one. I am also working through these notes for useful tools for navigating issues with constraints.

leftaroundabout commented 1 year ago

I'm afraid I won't have time to properly think about this in the next weeks, but eventually I will!

leftaroundabout / constrained-categories

Constraints and defining `foldMap` for a free category? #9