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
.
CodePudding user response:
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
CodePudding user response:
Yes, but not usefully. Without changing twice
's implementation, you can change its type. If you change its type to require a function which acts specifically like swap
(i.e., that it flips the order of type arguments to some type constructor, without caring about the details of those type arguments), then you can compose that function with itself.
{-# LANGUAGE RankNTypes #-}
twice :: (forall a b. f a b -> f b a) -> f a b -> f a b
twice f = f . f
> :t twice swap
twice swap :: (a, b) -> (a, b)
You can't use this for flip
directly, because currying associates the type parameters in the wrong order for us. But you can use a newtype to reorder things if you're explicit about the function being two-argument:
newtype BiFunction r a b = BiFunction {unBi :: a -> b -> r}
flipBi = BiFunction . flip . unBi
> :t twice flipBi
twice flipBi :: BiFunction r a b -> BiFunction r a b
The problem is that this makes twice
pretty useless for any other task. You can no longer write twice succ
to get a function that adds 2, for example, because succ
doesn't have this property that it reorders type parameters. twice f
is almost required to be the identity function, because it can't inspect or modify the values of type a
or b
at all. It can change the context in f
, though, so you could define someFunction
, Pair
, and Empty
such that twice someFunction (Pair 1 2) = Empty
. Give it a try if you think it'd be an interesting exercise.