How to work with types that change under composition?

Question

I recently read the very interesting paper Monotonicity Types in which a new HM-language is described that keeps track of monotonicity across operations, so that the programmer does not have to do this manually (and fail at compile-time when a non-monotonic operation is passed to something that requires one).

I was thinking that it probably would be possible to model this in Haskell, since the sfuns that the paper describes seem to be 'just another Arrow instance', so I set out to create a very small POC.

However, I came across the problem that there are, simply put, four kinds of 'tonicities' (for lack of a better term): monotonic, antitonic, constant (which is both) and unknown (which is neither), which can turn into one-another under composition or application:

When two 'tonic functions' are applied, the resulting tonic function's tonicity ought to be the most specific one that matches both types ('Qualifier Contraction; Figure 7' in the paper):

• if both are constant tonicity, the result should be constant.
• if both are monotonic, the result should be monotonic
• if both are antitonic, the result should be antitonic
• if one is constant and the other monotonic, the result should be monotonic
• if one is constant and the other antitonic, the result should be antitonic
• if one is monotonic and one antitonic, the result should be unknown.
• if either is unknown, the result is unknown.

When two 'tonic functions' are composed, the resulting tonic function's tonicity might flip ('Qualifier Composition; Figure 6' in the paper):

• if both are constant tonicity, the result should be constant.
• if both are monotonic, the result should be monotonic
• if both are antitonic, the result should be monotonic
• if one is monotonic and one antitonic, the result should be antitonic.
• if either is unknown, the result is unknown.

I have a problem to properly express this (the relationship between tonicities, and how 'tonic functions' will compose) in Haskell's types. My latest attempt looks like this, using GADTs, Type Families, DataKinds and a slew of other type-level programming constructs:

{-# LANGUAGE GADTs, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, UndecidableInstances, KindSignatures, DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
module Main2 where

import qualified Control.Category
import Control.Category (Category, (>>>), (<<<))

import qualified Control.Arrow
import Control.Arrow (Arrow, (***), first)


main :: IO ()
main =
  putStrLn "Hi!"

data Tonic t a b where
  Tonic :: Tonicity t => (a -> b) -> Tonic t a b
  Tonic2 :: (TCR t1 t2) ~ t3 => Tonic t1 a b -> Tonic t2 b c -> Tonic t3 a c

data Monotonic = Monotonic
data Antitonic = Antitonic
class Tonicity t

instance Tonicity Monotonic
instance Tonicity Antitonic

type family TCR (t1 :: k) (t2 :: k) :: k where
  TCR Monotonic Antitonic = Antitonic
  TCR Antitonic Monotonic = Antitonic
  TCR t t = Monotonic


--- But now how to define instances for Control.Category and Control.Arrow?

I have the feeling I am greatly overcomplicating things. Another attempt I had introduced

class (Tonicity a, Tonicity b) => TonicCompose a b where
  type TonicComposeResult a b :: *

but it is not possible to use TonicComposeResult in the instance declaration of e.g. Control.Category ("illegal type synonym family application in instance").

---

What am I missing? How can this concept properly be expressed in type-safe code?

Burble

I think this has to be re-thought. Tonic t :: * -> * -> * has the right kind for Arrow or Category, but Tonic Antitonic is not a category since the composition of two (antitonic) arrows is no longer an (antitonic) arrow. Indeed, antitonic functions do not make a category. At best, we can make a category with "functions of known tonicity", using a type which does not expose the tonicity (a sort of existential type) and juggle between Tonicity t a b (not a category) and SomeTonicity a b (category). Alternatively, we could use a IndexedCategory class to allow for tonicity changes. – Kero

@Kero very interesting! Can you elaborate on how a IndexedCategory class would work? – Burble

Something like class IC k where type F k t1 t2 ; type B k ; comp :: k t1 a b -> k t2 b c -> k (F k t1 t2) a c ; id :: k (B k) a c, I guess, forcing k to define the composition rule for indices ts (and the index for id). This is untested, it might require some more changes. – Kero

@Kero The other option you mention, is that similar to moving between GHC.TypeLits' KnownNat n and SomeNat? – Burble

Roughly, yes. I'd rather use two types instead of a typeclass like KnownNat, but the spirit is similar. This is assuming that you really want/need to reuse the standard arrow/category class, – Kero

@Kero actually, this makes me think. Arrows were first introduced as generalization of Monads because there were instances of them whose type specifications did not completely match up. Is there a more general Arrow-like interface waiting from the shadows that might be useful for cases like these, where the return type of composition might fill in a different t? – Burble

I believe there might indeed be such a generalization, extending IC above to arrows. Anyway, many standard typeclasses over the years have been extended/generalized in the libraries, but only a few of such generalizations proved useful enough to become widespread. This however does not mean that one should not experiment and have some fun ;) – Kero

@Kero Very cool! So we have (a) change between a general (non-category) type and more specialized types that are not parametrized by t (but can also not compose in the same way because they are restricted categories?). (b) convert between a general and an existential type that does not expose t, but then there is no way to convert back. (Is this true?). (c) Usage of an IndexedCategory. Exactly how this would solve the problem I don't know yet, because I'd think that would hit the same limits as my attempt above(?) (Please post an answer!) or (d) hand-roll a more general Category and Arrow. – Burble

The code I finally ended up with (with a simpler example that working with tonicities) can be found in this gist. It is based on the answer by Li-Yao Xia, and also contains the helper 'indexed category' and 'indexed arrow' typeclasses suggested by @chi. – Burble

Answer 1

The universe of tonicities is fixed, so a single data type would be more accurate. The data constructors are lifted to the type level with the DataKinds extension.

data Tonicity = Monotone | Antitone | Constant | Unknown

Then, I would use a newtype to represent tonic functions:

newtype Sfun (t :: Tonicity) a b = UnsafeMkSfun { applySfun :: a -> b }

To ensure safety, the constructor must be hidden by default. But users of such a Haskell EDSL would most likely want to wrap their own functions in it. Tagging the name of the constructor with "unsafe" is a nice compromise to enable that use case.

Function composition literally behaves as function composition, with some extra type-level information.

composeSfun :: Sfun t1 b c -> Sfun t2 a b -> Sfun (ComposeTonicity t1 t2) a c
composeSfun (UnsafeMkSfun f) (UnsafeMkSfun g) = UnsafeMkSfun (f . g)

-- Composition of tonicity annotations
type family ComposeTonicity (t1 :: Tonicity) (t2 :: Tonicity) :: Tonicity where
  ComposeTonicity Monotone Monotone = Monotone
  ComposeTonicity Monotone Antitone = Antitone
  ...
  ComposeTonicity _ _ = Unknown  -- Any case we forget is Unknown by default.
                                 -- In a way, that's some extra safety.

Boleslaw

Nothing unsafe about applySfun! Might also be worth just reusing Tagged. – Salute

Very good point! I still think Sfun should be its own opaque type though, while I think the point of Tagged is to be transparent. – Boleslaw