How to define an existential type with a constraint

Help
#1

Hi everyone,

In 3474 I was having trouble defining an existential type as follows:

class C a where
  f :: a -> Unit

data Any = Any (forall a. C a => a)

instance anyC :: C Any where
  f (Any a) = f a  -- (1)

This gives a compiler error. Then, Liam remarked the following:

The type forall a . C a => a means that a user of a term of this type gets to pick which a they want. Which is why Any 3 doesn’t make any sense: you “the implementer” can’t pick the a to be Int if the caller must pick it.

However, I have doubts about this, because with existentials the notion of “user” is a bit more nuanced. Namely, I would expect that a concrete a can be picked when introducing Any and cannot when eliminating. That is, Any 3 should be OK (given an instance C Int) and f above should only know that there is an instance C a and no more. The above program is perfectly fine in Haskell, modulo syntax, so I suspect that forall inside constructors works differently in PureScript?

1 Like
#2

Furthermore, providing a type annotation at (1) like this

instance anyC :: C Any where
  f (Any (a :: forall a. C a => a)) = f a

results in a compiler error which makes me wonder whether there is a bug somewhere:

Could not match constrained type

C a0 => a0

with type

C a0 => a0
…

Is this error OK?

#3

Two quick comments:

  • Does the Haskell code you’re referring to look like data Any = forall a. C a => Any a? (with the forall before the type constructor?) If so, that’s something different – it really is an existential type, but it’s special syntax for that. PS doesn’t support that syntax … Would you agree that forall a. C a => a is an universal type by itself? Then it will operate the same inside a datatype.
  • The “could not match constrained type with constrainted type” issue is well known. Basically, the compiler can’t decide higher-order polymorphism (aka nested foralls), so it doesn’t even try, which is unfortunate, as even a few simple cases (like this) would be helpful. Most of the time it can be worked around via eta-expansion: (\a -> f a) :: forall a. C a => a (because then the compiler introduces the a variable as a skolem, and then it can choose the inner one to unify with that “chosen” a).
1 Like
#4

Yes, I am indeed referring to ExistentialQuantification. Thanks for confirming my suspicion that that extension is a bit different than this case. Also, thanks for the explanation about type checking. The error message remains unfortunate though, because “symbolically” it shows a trivial situation…

#5

@monoidmusician

  • Most of the time it can be worked around via eta-expansion: (\a -> f a) :: forall a. C a => a (because then the compiler introduces the a variable as a skolem, and then it can choose the inner one to unify with that “chosen” a ).

I dont understand

how to use eta-expansion to help me implement Show instance here

module Test where

import Effect
import Effect.Console
import Prelude
import Data.Foldable
import Data.Show
import Unsafe.Coerce

newtype Showable = Showable (forall a . Show a => a)

mkShowable :: ∀ a. Show a => a -> Showable
mkShowable a = Showable a

instance showShowable :: Show Showable where
  -- this doesnt work
  show (Showable a) = ((\x -> show x) :: forall x . Show x => x -> String) a

  {-
    31    show (Showable a) = ((\x -> show x) :: forall x . Show x => x -> String) a
                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    No type class instance was found for

      Data.Show.Show t0

    The instance head contains unknown type variables. Consider adding a type annotation.

    while applying a function \$dictShow1 ->
                                \x ->
                                  (show (...)) x
      of type Show t0 => t0 -> String
      to argument a
    while checking that expression (\x ->
                                      show x
                                   )
                                   a
      has type String
    in value declaration showShowable

    where t0 is an unknown type
   -}


  -- nor this
  -- show (Showable a) = ((\(x :: forall xtype . Show xtype => xtype) -> show x)) a

  {-
    31    -- show (Showable a) = ((\x -> show x) :: forall x . Show x => x -> String) a


    No type class instance was found for

      Data.Show.Show t0

    The instance head contains unknown type variables. Consider adding a type annotation.

    while applying a function \$dictShow2 ->
                                \x ->
                                  (show (...)) x
      of type Show t0 => t0 -> String
      to argument a
    while checking that expression (\x ->
                                      show x
                                   )
                                   a
      has type String
    in value declaration showShowable
   -}

showables :: Array Showable
showables = [mkShowable 1, mkShowable unit, mkShowable "hello"]

main :: Effect Unit
main = do
  log $ intercalate ", " (map show showables)
#6

Your Showable should be something like:

newtype Showable = Showable (forall r. (forall a. Show a => a -> r) -> r)

mkShowable :: forall a. Show a => a -> Showable
mkShowable a = Showable \k -> k a

unShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
unShowable k1 (Showable k2) = k2 k1

test1 = mkShowable 42
test2 = unShowable (\a -> show a) test1
4 Likes
#7

ah, ok, this is where we have eta expansion, question closed :slight_smile: