CODEWITHSUNDEEP
haskelltypeclassexistential-typeconstraint-kinds
Rehno Lindeque
Rehno Lindeque

Reputation: 4435

How to abstract constraints in function with Rank-2 type?

The following snippet of code borrows from the Haskell wiki to carry around a typeclass dictionary along with an existential type:

{-# language ExistentialQuantification #-}
module Experiment1 where

data Showable = forall x. Show x => Showable x
instance Show Showable where showsPrec p (Showable x) = showsPrec p x

resultStr :: String
resultStr = show (Showable ()) -- "()"

Is it possible to write a function f :: (forall x. x -> result) -> result that is able to take the Showable constructor (or any other data constructor to an existential type) as an argument?

One failed attempt at doing this looks like this:

{-# language ExistentialQuantification, RankNTypes, ConstraintKinds #-}

module Experiment2 where

-- import Data.Constraint (Dict(..), withDict)

data Showable = forall x. Show x => Showable x
instance Show Showable where showsPrec p (Showable x) = showsPrec p x

f :: (cxt (), cxt result) => (forall x. cxt x => x -> result) -> result
f mkResult = mkResult ()

resultStr :: String
resultStr = show (f Showable)

As implied by my commented import above, I have the impression that the constraints package might allow me to pass around the necessary proofs, but I can't see how that would work?

Upvotes: 1

Views: 101

Answers (2)

Rehno Lindeque
Rehno Lindeque

Reputation: 4435

I apologize for posting my own answer, but this is another alternative I ended up finding:

{-# language ExistentialQuantification, RankNTypes, ConstraintKinds, KindSignatures, TypeFamilies, FlexibleInstances #-}

module Experiment3 where

import GHC.Exts

data Showable (cxt :: * -> Constraint) = forall x. (cxt ~ Show, cxt x) => Showable x
instance Show (Showable Show) where showsPrec p (Showable x) = showsPrec p x

f :: cxt () => (forall x. cxt x => x -> result cxt) -> result cxt
f mkResult = mkResult ()

resultStr :: String
resultStr = show (f Showable :: Showable Show)

Unfortunately it requires an explicit type signature in show (f Showable) while my goal was to get type inference (or rather, some kind of constraint inference) through Showable. So this answer is not a solution as such, but rather another counter example to what I wanted.

I will accept the answer by Cirdec since it guided me to this conclusion.

Upvotes: 0

Cirdec
Cirdec

Reputation: 24156

Your failed attempt works if you provide a way to determine cxt

import Data.Proxy

f :: (cxt (), cxt result) => p cxt -> (forall x. cxt x => x -> result) -> result
f _ mkResult = mkResult ()

resultStr :: String
resultStr = show (f (Proxy :: Proxy Show) Showable)

Upvotes: 1

Related Questions