Abstracting existential types

Learn
1

In our codebase we currently have several existential type of the form

data Foo a b = Foo ...

data SomeFoo = forall a b. SomeFoo (Foo a b)

useSomeFoo :: (forall a b. Foo a b -> c) -> SomeFoo -> c

This is some quite repetitive code and we’re currently using with several pyramid of dooms like

useSomeFoo
  (\foo -> useSomeBar
    (\bar -> useSomeBaz
      (\baz -> ...)
      bar.baz
    )
    foo.bar    
  )
  someFoo

To alleviate this we’re looking into ways to abstract this away.
To start, we would like do define something like

class Some t where
   type SomeT t

   useSome :: (forall a. t a -> c) -> SomeT t -> c

This fails when we try to write instance Some Foo because Foo has two type parameters, while, in the definition of Some, t is required to have only one.

We noticed that we could work around this issue by rewriting Foo as

data Foo' (c :: (Type, Type))

but I was wondering if there were more generic way to approach the issue.

Any other suggestion is welcome

2

Is useSomeFoo really just doing a pattern match? Then you can simply rewrite your pyramid like this:

  case someFoo of
    SomeFoo (Foo { bar = SomeBar (Bar { baz = SomeBaz baz }) }) -> ...
1 Like
3

I suspect this may be an XY problem. Perhaps if you explain what the code does you can get help to find a simpler implementation?

Regarding your question, you can define a different data type for each number of type variables. Something like this:

data Some1 f = forall a. Some1 (f a)

useSome1 :: (forall a. f a -> r) -> Some1 f -> r
useSome1 k (Some1 f) = k f

data Some2 f = forall a b. Some2 (f a b)

useSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
useSome2 k (Some2 f) = k f

data Some3 ...
4

thanks @jaror and @lortabac

I guess pattern matching would solve most of the cases, but probably not all of them if there are function calls involved.

Using Some1, Some2 would help reducing duplication.

The end goal here would be able to write something like (similarly to what ContT does)

Some.do
   foo <- ... 
   bar <- ...
   baz <- ...
   pure ...

where Some.>>= is using useSome to extract the value in the constructor of the existential type

To do this I guess having Some1, Some2, … would be an issue and it would require having a single Some instead

5

If you flip the arguments of your use... functions you can lay out code like this:

useSomeFoo someFoo \foo ->
useSomeBar foo.bar \bar ->
useSomeBaz bar.baz \baz ->
...
2 Likes
6

I fear that (f)ourmolu would get in the way of such a layout

7

How about using the Identity monad?

data Foo = forall a. Foo a
data Bar = forall b. Bar b
data Baz = forall c. Baz c

stuff :: Foo -> Bar -> Baz -> ()
stuff foo bar baz = runIdentity do
    Foo a <- pure foo
    Bar b <- pure bar
    Baz c <- pure baz
    pure ()
1 Like
8

They may require increasing indentation, but at least that serves to show the scope and lets you avoid ()s.

9

If you are not bothered by a slight performance and verbosity overhead, you can try something like this:

{-# LANGUAGE GADTs #-}

module Some
  ( Some (..),
    Uncurry (..),
    some2,
    fail,
    (>>=),
  )
where

import Prelude hiding ((>>=))

data Some f = forall a. Some (f a)

(>>=) :: Some f -> (forall a. f a -> r) -> r
(Some x) >>= k = k x

data Uncurry f t where
  UC :: {getUncurry :: f a b} -> Uncurry f (a, b)

some2 :: f a b -> Some (Uncurry f)
some2 x = Some (UC x)

{-# LANGUAGE GADTs #-}
{-# LANGUAGE QualifiedDo #-}

import Some

data Foo1 a = Foo1 Int

data Foo2 a b = Foo2 Int

test :: Int
test = Some.do
  Foo1 n <- Some (Foo1 1)
  UC (Foo2 m) <- some2 (Foo2 2)
  n + m
10

If they are:

1 Like
11

This in all very interesting!

The last thing which I’m not sure how to handle are constraints.

Consider

data Foo a where
  Foo :: Bar a => Int -> Foo a

data SomeFoo = forall a. Bar a => SomeFoo (Foo a)

useSomeFoo :: (forall a. Bar a => Foo a -> b) -> SomeFoo -> b

If I used Some and withSome from Data.Some instead, I wouldn’t be able to encode the Bar a constraint.

Is there a way to circumvent this issue and encode the constraint in Some?

12

The constraint is already provided by Foo; putting it in SomeFoo is just duplication. You can use a constraint-agnostic Some Foo and recover the constraint by pattern matching on Foo i.

2 Likes
13

This approach with pattern matching works almost perfectly.

There is still one case where I’m not sure how to make it work.

If I have a foo :: Foo a I can retrieve the Bar a constraint just by pattern matching on foo. But if I have a mFoo :: Maybe (Foo a), how can I retrieve the constraint on a? If I pattern match, I can obtain the constraint only for the Just case, and I’m stuck in the Nothing case.

One way out I see is defining something like

data MaybeFoo a where
  NothingFoo :: Bar a => MaybeFoo a
  JustFoo :: Bar a => Int -> Foo a

but it doesn’t feel the best way to go.

A concrete example of the issue is Haskell Playground

14

It’s not clear to me that the solution to the concrete example is not just to have foo take an explicit IsCurrency to constraint, like convert.

That said, you can always factor out your Bar constraint into another type and pair it up when necessary.

{-# LANGUAGE GHC2021, NoStarIsType, PatternSynonyms #-}

module FooBar where

import Data.Functor.Product
import Data.Functor.Compose
type (.) = Compose
type (*) = Product
infixr 9 .
infixr 8 *

data Some f where
  Some :: f a -> Some f

data Sat c a where
  Sat :: c a => Sat c a

{-# COMPLETE PS #-}
pattern PS :: () => c a => f a -> (Sat c * f) a
pattern PS fx = Pair Sat fx

{-# COMPLETE PSC #-}
pattern PSC :: () => c a => f (g a) -> (Sat c * f . g) a
pattern PSC fgx = PS (Compose fgx)


class Bar (a :: k)

-- Remove `Bar` constraint from `Foo`.
data Foo (a :: k) where
  Foo :: Int -> Foo a

-- Instead pair the `Bar` constraint with whatever transformation of `Foo`.
type FooBar k f = Sat Bar * f . Foo @k

-- The types have the right shape for `Some`.
eg :: Some (FooBar k f) -> (forall (a :: k). Bar a => f (Foo a) -> r) -> r
eg (Some (PSC ffx)) k = k ffx

Edit

Another approach would be to capture a quantified constraint in ExchangeRate:

data ExchangeRate from to where
  ER :: (IsCurrency from => IsCurrency to) => ExchangeRate from to

Then neither convert nor foo require IsCurrency constraints.

1 Like