Local instances in Haskell. Very WIP. Not intended for serious use.

LocalInstances.hs

{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, KindSignatures, MagicHash, TypeFamilies, AllowAmbiguousTypes, TypeApplications, FlexibleContexts, GADTs #-}

module LocalInstances where

import Control.Applicative
import Data.Bifunctor
import Data.List.NonEmpty
import Control.Arrow
import Data.Semigroup

import GHC.Exts
import Unsafe.Coerce

{-

Uses:

- Providing local instances that are restricted within a scope; and thus aren't exported.
- Making people mad.


Local Instances are meant to be used together with FlexibleContexts, TypeApplication, And AllowAmbiguousTypes.

OBS:
This quite obviously breaks the open-world assumption that modules such as Data.Set and Data.Map make use of. Overriding instances aren't without issues.


WARNING: This module makes use of GHC-implementation-dependant details. It's very unsafe.
In particular, it's sensitive to changes within the type-classes you make local instances of.
Therefore, don't actually use this.

Inspired by Edward Kmett's 'reflection' in order to create his greatest nightmare: local instances.

-}

data Dict c where
    Dict :: c => Dict c

class Localizable (c :: Constraint) where
    type InstanceDecl c
    toDict   :: InstanceDecl c -> Dict c
    toDict = unsafeToDict @c

    fromDict :: Dict c -> InstanceDecl c
    fromDict = unsafeFromDict @c


invoke :: Dict c -> (c => r) -> r
invoke Dict k = k

localize :: forall c r. Localizable c => InstanceDecl c -> (c => r) -> r
localize = invoke . toDict @c

instance Localizable (Num a) where
    type InstanceDecl (Num a) = LocalNum a

data LocalNum a = LocalNum {
        (-+#)           :: a -> a -> a
    ,   (--#)           :: a -> a -> a
    ,   (-*#)           :: a -> a -> a
    ,   _negate#        :: a -> a
    ,   _abs#           :: a -> a
    ,   _signum#        :: a -> a
    ,   _fromInteger#   :: Integer -> a
    }

instance Localizable (Semigroup a) where
    type InstanceDecl (Semigroup a) = LocalSemigroup a

data LocalSemigroup a = LocalSemigroup {
        (-<>#) :: a -> a -> a
    ,   _stimes# :: forall b. Integral b => b -> a -> a
    ,   _sconcat# :: NonEmpty a -> a
    }




-- Example dictionaries

firstSemigroup :: forall a. Dict (Semigroup a)
firstSemigroup = unsafeToDict $ LocalSemigroup @a const stimesIdempotent ( \ ~(x :| _) -> x )

numApp :: (Applicative f, Num b) => Dict (Num (f b))
numApp = toDict LocalNum{
        (-+#)           = liftA2 (+)
    ,   (--#)           = liftA2 (-)
    ,   (-*#)           = liftA2 (*)
    ,   _negate#        = fmap negate
    ,   _abs#           = fmap abs
    ,   _signum#        = fmap signum
    ,   _fromInteger#   = pure . fromInteger
    }


numTuples :: (Num a, Num b) => Dict (Num (a, b))
numTuples = toDict LocalNum{
        (-+#)           = \ ~(a1, b1) ~(a2, b2) -> (a1 + a2, b1 + b2)
    ,   (--#)           = \ ~(a1, b1) ~(a2, b2) -> (a1 - a2, b1 - b2)
    ,   (-*#)           = \ ~(a1, b1) ~(a2, b2) -> (a1 * a2, b1 * b2)
    ,   _negate#        = bimap negate negate
    ,   _abs#           = bimap abs abs
    ,   _signum#        = bimap signum signum
    ,   _fromInteger#   = fromInteger &&& fromInteger
    }

-- Example of use.

exampleOfUse :: (Int, Int)
exampleOfUse = case numTuples @Int @Int of Dict -> playingTuples (1, 3) (2, 7)

playingTuples :: Num (a, b) => (a, b) -> (a, b) -> (a, b)
playingTuples a b = negate $ (3 * a - b) + 10

-- Due to Semigroup becoming a superclass of Monoid, the below won't work for GHC versions 8.4 and above. Shows how fragile this system really is.

instance Localizable (Monoid a) where
    type InstanceDecl (Monoid a) = LocalMonoid a

data LocalMonoid a = LocalMonoid {
        localMempty     :: a
    ,   localMappend    :: a -> a -> a
    ,   localMconcat    :: [a] -> a
    }


localMonoid :: a -> (a -> a -> a) -> LocalMonoid a
localMonoid mempty' mappend' = LocalMonoid mempty' mappend' (foldr mappend' mempty')

appMonoid :: forall f a. (Applicative f, Monoid a) => Dict (Monoid (f a))
appMonoid = toDict (localMonoid (pure mempty) (liftA2 mappend))

sumMonoid :: forall a. Num a => Dict (Monoid a)
sumMonoid = toDict (LocalMonoid 0 (+) sum)

productMonoid :: forall a. Num a => Dict (Monoid a)
productMonoid = toDict (LocalMonoid 1 (*) product)

exampleOfUse1 :: forall a. Monoid a => [a] -> [a] -> [a]
exampleOfUse1 l r = localize @(Monoid [a]) (localMonoid [mempty ::a] (liftA2 mappend)) (l `mappend` r)

exampleOfUse2Aux :: Monoid (Maybe [Bool]) => Maybe [Bool]
exampleOfUse2Aux = do
  res <- mempty
  return $ res `mappend` [True, False, True]


-- This doesn't work. I'm still trying to figure out superclasses
{-
instance Localizable (Alternative f) where
    type InstanceDecl (Alternative f) = LocalAlternative f

data LocalAlternative f = LocalAlternative {
        _fmap#          :: forall a b. (a -> b) -> f a -> f b
    ,   (-<$#)          :: forall a b. b -> f a -> f b
    ,   _pure#          :: forall a. a -> f a
    ,   (-<*>#)         :: forall a b. f (a -> b) -> f a -> f b
    ,   _liftA2#        :: forall a b c. (a -> b -> c) -> f a -> f b -> f c
    ,   (-*>#)          :: forall a b. f a -> f b -> f b
    ,   (-<*#)          :: forall a b. f a -> f b -> f a
    ,   _empty#         :: forall a. f a
    ,   (-<|>#)         :: forall a. f a -> f a -> f a
    ,   _some#          :: forall a. f a -> f [a]
    ,   _many#          :: forall a. f a -> f [a]
    }

altZipList :: Dict (Alternative ZipList)
altZipList = toDict $ LocalAlternative fmap (<$) pure (<*>) liftA2 (*>) (<*) empty' (<|>-) some' many' where
    empty' = ZipList []
    ZipList as' <|>- ZipList bs' = ZipList $ go as' bs' where
      go [] b = b
      go a [] = a
      go (a:as) (_:bs) = a : go as bs

    some' v = some_v
      where
        many_v = some_v <|>- pure []
        some_v = fmap (:) v <*> many_v

    many' v = many_v
      where
        many_v = some_v <|>- pure []
        some_v = fmap (:) v <*> many_v

-}

-- Unsafe stuff.

newtype LocalInstance i r = LocalInstance (i => r)

data Unit a = Unit { fromUnit :: a } -- Not newtype.

unsafeLocalize :: forall c r k. k -> (c => r) -> r
unsafeLocalize k f = unsafeCoerce (LocalInstance f :: LocalInstance c r) k

unsafeToDict :: forall c k. k -> Dict c
unsafeToDict = unsafeCoerce (LocalInstance Dict :: LocalInstance c (Dict c))

unsafeFromDict :: forall c k. Dict c -> k
unsafeFromDict d = fromUnit (unsafeCoerce d)





-- This is for the future, once QuantifiedConstraints arrive.
{-

-- A dictionary that defines Num, Fractional, and Floating instances for a specific Applicative. (Use type application to specify which.)
appNum :: Applicative f => Dict (LiftedInstance f Num, LiftedInstance f Fractional, LiftedInstance f Floating)


-- A dictionary that defines Semigroup and Monoid instances for a specific Applicative. (Use type application to specify which.)
appMonoid :: Applicative f => Dict (LiftedInstance f Semigroup, LiftedInstance f Monoid)


type LiftedInstance f constr = forall a. constr a => constr (f a)

numTuples :: Dict (TupleInstances Num, TupleInstances Fractional, TupleInstances Floating)
type TupleInstances constraint =
    forall a b. (constraint a, constraint b) => constraint (a, b),
    forall a b c. (constraint a, constraint b, constraint c) => constraint (a, b, c),
    forall a b c d. (constraint a, constraint b, constraint c, constraint d) => constraint (a, b, c, d),
    forall a b c d e. (constraint a, constraint b, constraint c, constraint d, constraint e) => constraint (a, b, c, d, e),
    forall a b c d e f. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f) => constraint (a, b, c, d, e, f),
    forall a b c d e f g. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g) => constraint (a, b, c, d, e, f, g),
    forall a b c d e f g h. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h) => constraint (a, b, c, d, e, f, g, h),
    forall a b c d e f g h i. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i) => constraint (a, b, c, d, e, f, g, h, i),
    forall a b c d e f g h i j. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i, constraint j) => constraint (a, b, c, d, e, f, g, h, i, j),
    forall a b c d e f g h i j k. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i, constraint j, constraint k) => constraint (a, b, c, d, e, f, g, h, i, j, k),
    forall a b c d e f g h i j k l. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i, constraint j, constraint k, constraint l) => constraint (a, b, c, d, e, f, g, h, i, j, k, l),
    forall a b c d e f g h i j k l m. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i, constraint j, constraint k, constraint l, constraint m) => constraint (a, b, c, d, e, f, g, h, i, j, k, l, m),
    forall a b c d e f g h i j k l m n. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i, constraint j, constraint k, constraint l, constraint m, constraint n) => constraint (a, b, c, d, e, f, g, h, i, j, k, l, m, n),
    forall a b c d e f g h i j k l m n o. (constraint a, constraint b, constraint c, constraint d, constraint e, constraint f, constraint g, constraint h, constraint i, constraint j, constraint k, constraint l, constraint m, constraint n, constraint o) => constraint (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)

-}