2

I have some classes and their instances. The example shows some nonsensical classes. Their exact nature is not important.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}


class Foo a where
   foo :: a -> Int
class Bar a where
   bar :: a -> String

instance Foo Int where
   foo x = x
instance Foo String where
   foo x = length x

instance Bar Int where
   bar x = show x
instance Bar String where
   bar x = x

OK, now I want to create some existential types that hide these classes behind some datatype façade, so I don't have to deal with constraints. (I know existential types are considered an anti-pattern, please don't explain this to me).

data TFoo = forall a. Foo a => TFoo a
instance Foo TFoo where
  foo (TFoo x) = foo x
data TBar = forall a. Bar a => TBar a
instance Bar TBar where
  bar (TBar x) = bar x

Obviously there's some boilerplate in there. I want to abstract it away.

{-# LANGUAGE ConstraintKinds #-}
data Obj cls = forall o. (cls o) => Obj o

So instead of several existential types I have just one, parametrised by a typeclass. So far so good.

Now how do I perform operations on Obj a? The obvious attempt

op f (Obj a) = f a

fails because the type variable could escape.

existential.hs:31:18: error:
    • Couldn't match expected type ‘o -> p1’ with actual type ‘p’
        because type variable ‘o’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor:
          Obj :: forall (cls :: * -> Constraint) o. cls o => o -> Obj cls,
        in an equation for ‘call’
        at existential.hs:31:9-13
    • In the expression: f k
      In an equation for ‘call’: call f (Obj k) = f k
    • Relevant bindings include
        k :: o (bound at existential.hs:31:13)
        f :: p (bound at existential.hs:31:6)
        call :: p -> Obj cls -> p1 (bound at existential.hs:31:1)
   |
31 | call f (Obj k) = f k
   |                  ^^^
Failed, no modules loaded.

I kinda understand why this happens. But with real invocations like call foo and call bar the type variable wouldn't escape. Can I convince the compiler of it? Perhaps I somehow can express the type u -> v where v does not mention u (which really should be the type of f)? If not, what other ways to deal with the situation are there? I guess I could generate something with TemplateHaskell but I still cannot wrap my head around it.

lehins
  • 9,642
  • 2
  • 35
  • 49
n. m. could be an AI
  • 112,515
  • 14
  • 128
  • 243
  • 1
    Can you be more specific about what you're trying to do? What is `op`? – dfeuer Jul 01 '20 at 04:17
  • What you're doing is possible. There is a more detailed error somewhere in the code that you're not showing us. – luqui Jul 01 '20 at 04:41
  • 1
    @luqui this is the exact code I'm trying to compile, and this is the only error. – n. m. could be an AI Jul 01 '20 at 06:59
  • 1
    @dfeuer It is my attempt to explore a little object system (as in object-oriented programming) with subtyping. `op`, or rather `flip op`, would then be a method selector, like the `.` in `object . method` of a typical OOP language. I know this may not be the best way to do it... – n. m. could be an AI Jul 01 '20 at 07:03

1 Answers1

6

Your code works fine; the compiler just needs some help with its type.

Obj hides the type of its contents, which means that op's argument f must be polymorphic (that is, it can't scrutinise its argument). Turn on RankNTypes:

op :: (forall a. cls a => a -> r) -> Obj cls -> r
op f (Obj x) = f x

You have to give the type signature in full because GHC can't infer higher-rank types.

Existentially quantifying over a class like this is usually not the best way to design a given program.

Benjamin Hodgson
  • 42,952
  • 15
  • 108
  • 157