haskelltype-theory

How to write "twice" so it can accept "swap" without restricting their type

If I have these definitions

twice f = f . f

swap (x,y) = (y,x)

The type of twice is infered to (a -> a) -> a -> a and swap is infered to (a,b) -> (b,a).

If I write swap . swap the type of that expression is (a, b) -> (a, b).

But if I ask for twice swap its type is (a, a) -> (a, a).

I know that twice is restricting the type of swap. But I'm wondering if there is a way to write twice so that it accepts swap without restricting its type. That is, you can write twice swap and accept pairs where each component has a different type.

The same happens with flip :: (a -> b -> c) -> b -> a -> c, because twice flip :: (a -> a -> b) -> a -> a -> b.

Solution

  • This is tricky to do, because you need to express that the result- and argument types are polymorphic, yet in a particular functional relationship. You need to provide this relationship in an explicit way. The most common way of expressing a type-level function is with a type family, but such functions can not be named as first-class entities. Also they can't encode the bidirectional natural of type relations like in swap.

    What you can do instead is represent the function with a unique type-tag, and link the argument- and result types together with a MPTC.

    {-# LANGUAGE FunctionalDependencies, AllowAmbiguousTypes #-}

class PolyFun f a b | f a -> b, f b -> a where
  once :: a -> b

data Swap

instance PolyFun Swap (a,b) (b,a) where
  once = swap

    Now,

    {-# LANGUAGE ScopedTypeVariables, TypeApplications, UnicodeSyntax #-}

twice :: ∀ f a b c . (PolyFun f a b, PolyFun f b c) => a -> c
twice = once @f @b @c . once @f @a @b

    GHCi> twice @Swap (3, "hi")
(3,"hi")

    This is fairly versatile,

    {-# LANGUAGE FlexibleInstances      #-}

data Concat

instance PolyFun Concat [[a]] [a] where
  once = concat

data Flip

instance PolyFun Flip (a -> b -> c) (b -> a -> c) where
  once = flip

    GHCi> twice @Concat [ [[1,2,3],[4,5]], [[6,7],[8]] ]
[1,2,3,4,5,6,7,8]
GHCi> twice @Flip (/) 9 3
3.0

    but it has its limitations as well, in particular the way I wrote it above the argument and result of the function must be inferrable from each other. But for many functions, only the argument type can be inferred from the result type and not vice versa, or sometimes only the result type from the arguments. You would have to use different classes to cover all the possible ways the type information can flow, I don't think there's a single way that does it all automatically.

    Edit It turns out there is actually a single way that does it automatically, but, erm... don't try this at home, kids...

    {-# LANGUAGE FunctionalDependencies, AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications, UnicodeSyntax #-}
{-# LANGUAGE FlexibleInstances, DataKinds, PolyKinds, GADTs #-}
{-# LANGUAGE TypeFamilies, ConstraintKinds, FlexibleContexts #-}
{-# LANGUAGE RankNTypes, TypeOperators, UndecidableInstances #-}

import Data.Kind (Type, Constraint)

import Data.Tuple (swap)

import Data.These


class HasThis (t :: These k k) where
  type UseThis t :: k

instance HasThis ('This a) where
  type UseThis ('This a) = a
instance HasThis ('These a b) where
  type UseThis ('These a b) = a

class HasThat (t :: These k k) where
  type UseThat t :: k

instance HasThat ('That b) where
  type UseThat ('That b) = b
instance HasThat ('These a b) where
  type UseThat ('These a b) = b

data TheseSing (t :: These k k) where
  ThisS :: TheseSing ('This a)
  ThatS :: TheseSing ('That b)
  TheseS :: TheseSing ('These a b)

class TFun f where
  type Accepted f a :: Constraint
  type ($) f a :: Type

type TfnT = Type

class PolyFun f where
  type Inferences f :: These TfnT TfnT
  inferences :: TheseSing (Inferences f)
  once_fti :: ( HasThis (Inferences f)
              , TFun (UseThis (Inferences f))
              , Accepted (UseThis (Inferences f)) a
              )
                  => a -> (UseThis (Inferences f) $ a)
  once_rti :: ( HasThat (Inferences f)
              , TFun (UseThat (Inferences f))
              , Accepted (UseThat (Inferences f)) b
              )
                  => (UseThat (Inferences f) $ b) -> b

class ForwardInf i x y | i x -> y where
  usingThisFwd :: ∀ r .
       ( ( TFun i, Accepted i x
         , y ~ (i $ x) )
         => r ) -> r
instance ( TFun i, Accepted i x
         , y ~ (i $ x) )
      => ForwardInf i x y where
  usingThisFwd φ = φ

class ReverseInf i x y | i y -> x where
  usingThatRev :: ∀ r .
       ( ( TFun i, Accepted i y
         , x ~ (i $ y) )
         => r ) -> r
instance ( TFun i, Accepted i y
         , x ~ (i $ y) )
      => ReverseInf i x y where
  usingThatRev φ = φ

type family AnyTI infs :: Type -> Type -> Constraint where
  AnyTI ('This i) = ForwardInf i
  AnyTI ('That i) = ReverseInf i
  AnyTI ('These i e) = ForwardInf i

once :: ∀ f x y . (PolyFun f, AnyTI (Inferences f) x y) => x -> y
once = case inferences @f of
  ThisS -> usingThisFwd @(UseThis (Inferences f)) @x @y (once_fti @f @x)
  ThatS -> usingThatRev @(UseThat (Inferences f)) @x @y (once_rti @f @y)
  TheseS -> usingThisFwd @(UseThis (Inferences f)) @x @y (once_fti @f @x)

data Swap

type family SwapT t where
  SwapT (a,b) = (b,a)

class IsTuple t where
  type Fst t :: Type
  type Snd t :: Type
  deconstructTuple :: (t ~ (Fst t, Snd t) => r) -> r

instance IsTuple (a,b) where
  type Fst (a,b) = a
  type Snd (a,b) = b
  deconstructTuple φ = φ

instance TFun Swap where
  type ($) Swap t = SwapT t
  type Accepted Swap t = IsTuple t

fti_swap :: ∀ t . IsTuple t => t -> SwapT t
fti_swap = deconstructTuple @t swap

rti_swap :: ∀ t . IsTuple t => SwapT t -> t
rti_swap = deconstructTuple @t swap

instance PolyFun Swap where
  type Inferences Swap = 'These Swap Swap
  inferences = TheseS
  once_fti = fti_swap
  once_rti = rti_swap

data Compose f g

instance (TFun f, TFun g) => TFun (Compose f g) where
  type Accepted (Compose f g) a = (Accepted g a, Accepted f (g$a))
  type ($) (Compose f g) a = f $ (g$a)

class CompShared (a :: These Type Type) (b :: These Type Type) where
  type Shared a b :: These Type Type
  sharingFwd :: ∀ x r . ( HasThis (Shared a b)
                        , Accepted (UseThis (Shared a b)) x )
        => (( HasThis a, HasThis b
            , TFun (UseThis a), TFun (UseThis b)
            , Accepted (UseThis b) x
            , Accepted (UseThis a) (UseThis b $ x)
            , (UseThis (Shared a b) $ x) ~ (UseThis a $ (UseThis b $ x)) )
             => r) -> r
  sharingRev :: ∀ y r . ( HasThat (Shared a b)
                        , Accepted (UseThat (Shared a b)) y )
        => (( HasThat a, HasThat b
            , TFun (UseThat a), TFun (UseThat b)
            , Accepted (UseThat a) y
            , Accepted (UseThat b) (UseThat a $ y)
            , (UseThat (Shared a b) $ y) ~ (UseThat b $ (UseThat a $ y)) )
             => r) -> r
  shared :: TheseSing (Shared a b)

instance (TFun f, TFun g) => CompShared ('This f) ('This g) where
  type Shared ('This f) ('This g) = 'This (Compose f g)
  shared = ThisS
  sharingFwd φ = φ
  sharingRev _ = undefined

instance (TFun f, TFun g) => CompShared ('This f) ('These g c) where
  type Shared ('This f) ('These g c) = 'This (Compose f g)
  shared = ThisS
  sharingFwd φ = φ
  sharingRev _ = undefined

instance (TFun f, TFun g) => CompShared ('That f) ('That g) where
  type Shared ('That f) ('That g) = 'That (Compose g f)
  shared = ThatS
  sharingFwd _ = undefined
  sharingRev φ = φ

instance (TFun f, TFun g) => CompShared ('That f) ('These c g) where
  type Shared ('That f) ('These c g) = 'That (Compose g f)
  shared = ThatS
  sharingFwd _ = undefined
  sharingRev φ = φ

instance (TFun f, TFun g, TFun h, TFun i)
            => CompShared ('These f h) ('These g i) where
  type Shared ('These f h) ('These g i) = 'These (Compose f g) (Compose i h)
  shared = TheseS
  sharingFwd φ = φ
  sharingRev φ = φ

data Twice f

twice_fti :: ∀ f x .
       ( PolyFun f
       , CompShared (Inferences f) (Inferences f)
       , HasThis (Shared (Inferences f) (Inferences f))
       , Accepted (UseThis (Shared (Inferences f) (Inferences f))) x )
     => x -> (UseThis (Shared (Inferences f) (Inferences f)) $ x)
twice_fti = sharingFwd @(Inferences f) @(Inferences f) @x
               (once_fti @f . once_fti @f)

twice_rti :: ∀ f y .
       ( PolyFun f
       , CompShared (Inferences f) (Inferences f)
       , HasThat (Shared (Inferences f) (Inferences f))
       , Accepted (UseThat (Shared (Inferences f) (Inferences f))) y )
     => (UseThat (Shared (Inferences f) (Inferences f)) $ y) -> y
twice_rti = sharingRev @(Inferences f) @(Inferences f) @y
               (once_rti @f . once_rti @f)

instance (PolyFun f, CompShared (Inferences f) (Inferences f))
             => PolyFun (Twice f) where
  type Inferences (Twice f) = Shared (Inferences f) (Inferences f)
  inferences = shared @(Inferences f) @(Inferences f)
  once_fti = twice_fti @f
  once_rti = twice_rti @f

twice :: ∀ f x y . (PolyFun (Twice f), AnyTI (Inferences (Twice f)) x y) => x -> y
twice = once @(Twice f)

data FromInteger

instance TFun FromInteger where
  type Accepted FromInteger a = Integral a
  type ($) FromInteger a = Integer

instance PolyFun FromInteger where
  type Inferences FromInteger = That FromInteger
  inferences = ThatS
  once_fti = undefined
  once_rti = fromInteger

    GHCi> twice @Swap (1, "hi")
(1,"hi")
GHCi> twice @FromInteger 5
5