Defining ad-hoc polymorphism using dependently-typed implicits.

OpClasses.idr

-- This illustrates (most of) a new(?) encoding of ad-hoc polymorphism using
-- dependent types and implicits.
--
-- Benefits of this approach:
-- • can have multiple “ambiguous” instances without requiring things like
--   Haskell’s newtypes to distinguish them;
-- • can disambiguate instances with minimal information, rather than having to
--   know some arbitrary instance name as you would with a system like Scala’s
--   implicits;
-- • implementers don’t need to know/provide the full family of instances – they
--   can define only the basic properties of their operations and expect
--   aggregate structures to be made available automatically;
-- • new aggregate structures based on existing properties can be created
--   anywhere, and instances for previously-defined operations will be coalesced
--   as necessary without additional changes; and
-- • the “diamond problem” in inheritance-based systems is removed – if the
--   correct properties are specified, both `Monad` and `Traversable` can be
--   coalesced without either winding up with ambiguous `Functor` instances or
--   having to define a mega-instance like `Monad with Traversable`.
--
-- Tradeoffs:
-- • requires dependent types, so not as available or ergonomic in all languages
-- • relies on laws, which are sometimes difficult to prove and unfamiliar to
--   many programmers (although, you could make the propeties empty, where they
--   act as just a tag that that property is satisfied or use `postulate` to
--   make it an axiom that you don’t require proof of)
-- 
-- Written with assistance from (but not necessarily endorsement of)
-- @monoidmusician & @srdqty.
--
-- NB: This probably _overuses_ implicits beyond the maximum benefit we get from
--     them. Figuring out where we should have explicit parameters may simplify
--     some things.
module OpClasses

||| First, we define a type for each individual property (or law) that we care
||| about. These should be as atomic as possible.
|||
||| TODO: Not sure why these need to be `data` declarations instead of
|||       functions, but it currently helps with implicit resolution.

data Associative : {op : t -> t -> t} -> Type where
  MkAssociative : ((a : t) -> (b : t) -> (c : t) -> op a (op b c) = op (op a b) c)
               -> Associative {op}

data Commutative : {op : t -> t -> t} -> Type where
  MkCommutative : ((a : t) -> (b : t) -> op a b = op b a) -> Commutative {op}

data LeftIdentity : {op : t -> t -> t} -> {leftUnit : t} -> Type where
  MkLeftIdentity : ((a : t) -> op leftUnit a = a)
                -> LeftIdentity {op} {leftUnit}

data RightIdentity : {op : t -> t -> t} -> {rightUnit : t} -> Type where
  MkRightIdentity : ((a : t) -> op a rightUnit = a)
                 -> RightIdentity {op} {rightUnit}

data LeftCancellative : {op : t -> t -> t} -> Type where
  MkLeftCancellative
    : ((a : t) -> (b : t) -> (c : t) -> op a b = op a c -> b = c)
   -> LeftCancellative {op}

data RightCancellative : {op : t -> t -> t} -> Type where
  MkRightCancellative
    : ((a : t) -> (b : t) -> (c : t) -> op a c = op b c -> a = b)
   -> RightCancellative {op}

data LeftDistributive : {mul : t -> t -> t} -> {add : t -> t -> t} -> Type where
  MkLeftDistributive
    : ((a : t) -> (b : t) -> (c : t) -> mul a (add b c) = add (mul a b) (mul a c))
   -> LeftDistributive {mul} {add}

data RightDistributive : {mul : t -> t -> t} -> {add : t -> t -> t} -> Type where
  MkRightDistributive
    : ((a : t) -> (b : t) -> (c : t) -> mul (add a b) c = add (mul a c) (mul b c))
   -> RightDistributive {mul} {add}

||| • Structures are defined as records, with properties as fields.
||| • We use a function for the type to make the parameters to the record
|||   implicit and potentially to make other changes – e.g., in `Identity` we
|||   existentialize `unit` since it’s necessarily unique.
||| • We then use a function that specifies each of the components of the
|||   structure as an implicit. These can be either individual properties or
|||   other structures that are subsumed by the one being defined. This
|||   function, with all arguments implicit serves as an implicit search
|||   assistant.

record IdentityRec (t : Type) (op : t -> t -> t) (unit : t) where
    constructor IdentityInfo
    leftIdentity : LeftIdentity {op} {leftUnit=unit}
    rightIdentity : RightIdentity {op} {rightUnit=unit}

Identity : {op : t -> t -> t} -> Type
Identity {t} {op} = (unit : t ** IdentityRec t op unit)

%hint
resolveIdentity
  :  {auto l : LeftIdentity {op} {leftUnit=unit}}
  -> {auto r : RightIdentity {op} {rightUnit=unit}}
  -> Identity {op}
resolveIdentity {l} {r} = (_ ** IdentityInfo l r)

record CancellativeRec (op : t -> t -> t) where
    constructor CancellativeInfo
    leftCancellative : LeftCancellative {op}
    rightCancellative : RightCancellative {op}

||| NB: We could eliminate a lot of definitions like this if records took
|||     implicit parameters.
Cancellative : {op : t -> t -> t} -> Type
Cancellative {op} = CancellativeRec op

||| NB: And we could eliminate a lot of definitions like this if record
|||     constructors could take implicit parameters.
resolveCancellative
  :  {auto l : LeftCancellative {op}}
  -> {auto r : RightCancellative {op}}
  -> Cancellative {op}
resolveCancellative {l} {r} = CancellativeInfo l r

record DistributiveRec (mul : t -> t -> t) (add : t -> t -> t) where
    constructor DistributiveInfo
    leftDistributive : LeftDistributive {mul} {add}
    rightDistributive : RightDistributive {mul} {add}

Distributive : {mul : t -> t -> t} -> {add : t -> t -> t} -> Type
Distributive {mul} {add} = DistributiveRec mul add

%hint
resolveDistributive
  :  {auto l : LeftDistributive {mul} {add}}
  -> {auto r : RightDistributive {mul} {add}}
  -> Distributive {mul} {add}
resolveDistributive {l} {r} = DistributiveInfo l r

record SemigroupRec (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : Associative {op}

Semigroup : {op : t -> t -> t} -> Type
Semigroup {op} = SemigroupRec op

%hint
resolveSemigroup : {auto associative : Associative {op}} -> Semigroup {op}
resolveSemigroup {associative} = SemigroupInfo associative

record MonoidRec (t : Type) (op : t -> t -> t) (unit : t) where
    constructor MonoidInfo
    leftIdentity : LeftIdentity {op} {leftUnit=unit}
    rightIdentity : RightIdentity {op} {rightUnit=unit}
    associative : Associative {op}

Monoid : {op : t -> t -> t} -> Type
Monoid {t} {op} = (unit : t ** MonoidRec t op unit)

%hint
resolveMonoid
  : {auto semigroup : Semigroup {op}} -> {auto identity : Identity {op}} -> Monoid {op}
resolveMonoid {semigroup} {identity} =
  let (unit ** ident) = identity
  in (unit ** MonoidInfo (leftIdentity ident) (rightIdentity ident) (associative semigroup))

||| NB: We use implicit conversions to extract _unique_ substructures from
|||     larger structures. However, implicit conversions don’t chain, so we also
|||     need not only `groupToMonoid` but `groupToSemigroup` – this means there
|||     are more conversions defined than we’d like, but it also has some
|||     benefits.
|||     A language that had row types or subtypes could handle this
|||     automatically with either of those features.
implicit
monoidToSemigroup : Monoid {op} -> Semigroup {op}
monoidToSemigroup (_ ** monoid) =
  resolveSemigroup {associative=associative monoid}

record SemiringRec (add : t -> t -> t) (mul : t -> t -> t) where
    constructor SemiringInfo
    additive : Semigroup {op=add} -- should be commutative
    multiplicative : Monoid {op=mul}
    leftDistributive : LeftDistributive {mul} {add}
    rightDistributive : RightDistributive {mul} {add}

Semiring : {add : t -> t -> t} -> {mul : t -> t -> t} -> Type
Semiring {add} {mul} = SemiringRec add mul

%hint
resolveSemiring
  :  {auto distributive : Distributive {mul} {add}}
  -> {auto additive : Semigroup {op=add}}
  -> {auto multiplicative : Monoid {op=mul}}
  -> Semiring {add} {mul}
resolveSemiring {distributive} {additive} {multiplicative} =
  SemiringInfo
  additive
  multiplicative
  (leftDistributive  distributive)
  (rightDistributive distributive)

||| NB: Here we take advantage of the lack of implicit chaining.
|||    `semiringToMonoid` is unique, but `monoidToSemigroup . semiringToMonoid`
|||     wouldn’t be because there’s another (commutative) semigroup in the
|||     semiring.
implicit
semiringToMonoid : Semiring {mul} -> Monoid {op=mul}
semiringToMonoid semiring = multiplicative semiring

||| Now we can define operations that use our structures as constraints. Again,
||| encoded as implicit parameters.

combine3 : {auto semigroup : Semigroup {t} {op}} -> t -> t -> t -> t
combine3 {op} a b c = op a (op b c)

fold : {auto monoid : Monoid {t} {op}} -> List t -> t
fold {op} {monoid} ts = let (unit ** _) = monoid in foldr op unit ts

||| It’s also possible to have some properties implied by combinations of other
||| properties.

%hint
resolveLeftIdentity
  :  {auto commutative : Commutative {op}}
  -> {auto rightIdentity : RightIdentity {op} {rightUnit}}
  -> LeftIdentity {op} {leftUnit=rightUnit}
resolveLeftIdentity {rightUnit} {commutative=MkCommutative com} {rightIdentity=MkRightIdentity id} =
  MkLeftIdentity (\a => rewrite (com rightUnit a) in (id a))

%hint
resolveRightIdentity
  :  {auto commutative : Commutative {op}}
  -> {auto leftIdentity : LeftIdentity {op} {leftUnit}}
  -> RightIdentity {op} {rightUnit=leftUnit}
resolveRightIdentity {leftUnit} {commutative=MkCommutative com} {leftIdentity=MkLeftIdentity id} =
  MkRightIdentity (\a => rewrite (com a leftUnit) in (id a))

||| Then we prove _only_ the individual properties for each operation. These are
||| our “instances”, which we should really have a mechanism for guaranteeing
||| uniqueness of, and they shouldn’t have to be named.

%hint
addAssoc : Associative {op=Prelude.Nat.plus}
addAssoc = MkAssociative plusAssociative

%hint
addLeftIdent : LeftIdentity {op=Prelude.Nat.plus} {leftUnit=Z}
addLeftIdent = MkLeftIdentity plusZeroLeftNeutral

%hint
addCommutative : Commutative {op=Prelude.Nat.plus}
addCommutative = MkCommutative plusCommutative

||| Thanks to `resolveRightIdentity`, we don’t need to define `addRightIdent,
||| because it’s been implied by ``addLeftIdent` and `addCommutative`.

||| And, finally, we can call the constrained functions (`combine3` and `fold`)
||| on `Nat`s, and the aggregate “instances” on larger structures are
||| automatically built out of our individual implicit definitions of various
||| properties.

test_s : combine3 (S Z) (S (S Z)) (S (S (S Z))) = 6
test_s = Refl

test_m : fold [S Z, S (S Z), S (S (S Z))] = 6
test_m = Refl

||| But things can get ambiguous. Here we have a second associative operation on
||| Naturals.

%hint
mulAssoc : Associative {op=Prelude.Nat.mult}
mulAssoc = MkAssociative multAssociative

||| Unfortunately, Idris implicit search just looks backward for the closest
||| definition. So even though we have both `Semigroup {op=plus}` and
||| `Semigroup {op=mult}`, it finds the multiplication one. Ideally, this
||| wouldn’t compile, and we’d have to specify which one we want. Instead, it
||| will always use the multiplication one, and we’d need to explicitly specify
||| `plus` if we want to use that one.
test_s2 : combine3 (S (S Z)) (S (S Z)) (S (S (S Z))) = 12
test_s2 = Refl

||| If we had the uniqueness constraint we’d like, we’d have to specify the `op`:
test_s2b : combine3 {op=Prelude.Nat.plus} (S (S Z)) (S (S Z)) (S (S (S Z))) = 7
test_s2b = Refl

||| And sometimes we need to “extract” a smaller structure impllied by a larger
||| one. This can be explicit or implicit. Here, we pull out the distinct
||| semigroup and monoid from the semiring. We _should_ need to specify the
||| semigroup here (because both semiring operations form semigroups), but
||| _shouldn’t_ have to specify the monoid for `fold`, as only one of the
||| operations forms a monoid.

%hint
multLeftIdent : LeftIdentity {op=Prelude.Nat.mult} {leftUnit=S Z}
multLeftIdent = MkLeftIdentity multOneLeftNeutral

%hint
mulRightIdent : RightIdentity {op=Prelude.Nat.mult} {rightUnit=S Z}
mulRightIdent = MkRightIdentity multOneRightNeutral

%hint
mulLeftDist : LeftDistributive {mul=Prelude.Nat.mult} {add=Prelude.Nat.plus}
mulLeftDist = MkLeftDistributive multDistributesOverPlusRight

%hint
mulRightDist : RightDistributive {mul=Prelude.Nat.mult} {add=Prelude.Nat.plus}
mulRightDist = MkRightDistributive multDistributesOverPlusLeft

mixed : {auto semiring : Semiring {t}} -> t -> t -> List t -> t
mixed {semiring} x y =
    combine3 {semigroup=additive semiring} x y . fold

||| This is overconstrained, but it illustrates how we can take advantage of the
||| implicit conversions. `combine3` expects a `Semigroup`, but we provide it a
||| `Monoid` (and this _must_ be explicit, because there are multiple possible
||| semigroups in the context). The only available `Monoid` still gets used for
||| `fold`.
mixed_m : {auto semiring : Semiring {t}} -> t -> t -> List t -> t
mixed_m {semiring} x y =
    combine3 {semigroup=multiplicative semiring} x y . fold

test_sr : mixed (S (S Z)) (S (S Z)) [S Z, S (S Z), S (S (S Z))] = 10
test_sr = Refl

||| This shows how the `Monoid` is automatically converted to the `Semigroup`
||| needed by `combine3`.
|||
||| TODO: This shows a place we have to be careful (that we haven’t been careful
|||       with above). Notice in `Monoid {t} {op}`, we never use `op` elsewhere,
|||       so we shouldn’t need to call out that parameter. However, if we omit
|||       it, then `test_m2` can’t specify the operation to use for the monoid
|||       and would have to reify a monoid instance somehow. We have to be
|||       careful because it’s a problem that isn’t apparent until we try to
|||      _use_ `lessMixed`. We have a similar problem with `unit`, where there’s
|||       no way to expose the unit as a disambiguator (I don’t think), since
|||       it’s in the `Sigma` of the monoid.
lessMixed : {auto monoid : Monoid {t} {op}} -> t -> t -> List t -> t
lessMixed x y = combine3 x y . fold

test_m2 : lessMixed {op=Prelude.Nat.mult} 2 2 [1, 2, 3] = 24
test_m2 = Refl

WeakOpClasses.hs

{-# language ConstraintKinds
           , FlexibleContexts
           , FlexibleInstances
#-}

-- | This is a sort-of introductory version of operation classes. It lacks many
--   features, but is encodable in fairly vanilla Haskell, so is hopefully
--   fairly comprehensible. There are richer versions in Dependent Haskell and
--   other languages, but it is hopefully useful to understand some of the
--   concepts from this before looking into the deeper versions (which also have
--   to jump through more hoops because of various language limitations).
module WeakOpClasses where

import Prelude hiding (Monoid, product)
import Data.Kind (Type)
import Data.Monoid (Sum(..), Product(..))
import Numeric.Natural

-- | This type class gives us a place to put a single operation, without any
--   properties not implied by the type. This wouldn’t need to exist if the
--   operation could live in the parameters.
class Closed a where
  op :: a -> a -> a

-- @ These classes are empty. In a dependently-typed language, they would
--   contain the laws that require proofs, but here they are simply tags that
--  _assert_ that the property holds.

class Closed a => Associative a

class Closed a => Commutative a

class Closed a => LeftIdentity a where
  leftUnit :: a

class Closed a => RightIdentity a where
  rightUnit :: a

class (Closed (Sum a), Closed (Product a)) => LeftDistributive a

class (Closed (Sum a), Closed (Product a)) => RightDistributive a

type Identity a = (LeftIdentity a, RightIdentity a)

unit :: Identity a => a
unit = leftUnit
  
type Distributive a = (LeftDistributive a, RightDistributive a)
type Semigroup = Associative
type Monoid a = (Semigroup a, Identity a)
type CommutativeSemigroup a = (Commutative a, Semigroup a)
type CommutativeMonoid a = (Commutative a, Monoid a)
type Semiring a =
  (Distributive a, CommutativeSemigroup (Sum a), Monoid (Product a))
type Rig a = (Semiring a, CommutativeMonoid (Sum a))

instance Closed (Sum Natural) where
  op = (+)

instance Closed (Product Natural) where
  op = (*)


instance Associative (Sum Natural)
instance Commutative (Sum Natural)
instance LeftIdentity (Sum Natural) where
  leftUnit = 0
instance RightIdentity (Sum Natural) where
  rightUnit = 0

instance Associative (Product Natural)
instance Commutative (Product Natural)
instance LeftIdentity (Product Natural) where
  leftUnit = 1
instance RightIdentity (Product Natural) where
  rightUnit = 1

instance LeftDistributive Natural
instance RightDistributive Natural

combine3 :: Semigroup t => t -> t -> t -> t
combine3 x y z = op (op x y) z

fold :: Monoid t => [t] -> t
fold = foldr op unit

-- | FIXME: How do we select which `Monoid` we want to use in this case?
sum :: Rig t => [t] -> t
sum = getSum . fold . fmap Sum

-- | This one can _only_ use the multiplicative, as `fold` requires a `Monoid`
--   and a `Semiring` has only one of those. So we _shouldn’t_ need to tell the
--   compiler which instance we want, but because of the `newtype` hack, we do
--   need to.
product :: Semiring t => [t] -> t
product = getProduct . fold . fmap Product

mixed :: Semiring t => t -> t -> [t] -> t
mixed x y = getSum . combine3 (Sum x) (Sum y) . Sum . product

mixed_m :: Semiring t => t -> t -> [t] -> t
mixed_m x y = getProduct . combine3 (Product x) (Product y) . Product . product

lessMixed :: Monoid t => t -> t -> [t] -> t
lessMixed x y = combine3 x y . fold

My biggest issue with the current implementation of this is the approx. n(n-1)/2 implicit conversion definitions needed to handle the “subtyping” of structures. At the very least, it’s easy to forget some without noticing until a user manages to hit that exact case.

Also, the errors that come out when an instance isn’t available are generally terrible. In fact, sometimes non-sensical as far as I can tell.

Added a Haskell version that omits all the dependently-typed parts of the approach, but hopefully makes it accessible to a wider audience. It also falls back on the newtype instance hack, so it misses out on some of the “magic” instance resolution.