CODEWITHSUNDEEP
haskellgadtreflex
Wizek
Wizek

Reputation: 4993

(How) is it possible to have polymorphic values in a `dependent-map` GADT?

Anyone knows how/if it's possible to extend the Foo GADT in this code:

{-# language GADTs #-}
{-# language DeriveGeneric #-}
{-# language DeriveAnyClass #-}
{-# language TemplateHaskell #-}
{-# language StandaloneDeriving #-}

import Prelude                  (Int, String, print, ($))
import Data.GADT.Show           ()
import Data.GADT.Compare        ()
import Data.Dependent.Map       (DMap, fromList, (!))
import Data.Dependent.Sum       ((==>))
import Data.GADT.Compare.TH     (deriveGEq, deriveGCompare)
import Data.Functor.Identity    (Identity)

data Foo a where
  AnInt   :: Foo Int
  AString :: Foo String

deriveGEq      ''Foo
deriveGCompare ''Foo

dmap1 :: DMap Foo Identity
dmap1 = fromList [AnInt ==> 1, AString ==> "bar"]

main = do
  print $ dmap1 ! AnInt
  print $ dmap1 ! AString

  -- Prints:
  -- Identity 1
  -- Identity "bar"

with

  ANum :: Num n => Foo n

(or something similar) to allow for polymorphic values in a dependent-map?

When I try, I get a type error like this:

exp-dep-map.hs:20:1: error:
    • Couldn't match type ‘a’ with ‘b’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          geq :: forall a b. Foo a -> Foo b -> Maybe (a := b)
        at exp-dep-map.hs:20:1-20
      ‘b’ is a rigid type variable bound by
        the type signature for:
          geq :: forall a b. Foo a -> Foo b -> Maybe (a := b)
        at exp-dep-map.hs:20:1-20
      Expected type: Maybe (a := b)
        Actual type: Maybe (a :~: a)
    • In a stmt of a 'do' block: return Refl
      In the expression: do return Refl
      In an equation for ‘geq’: geq ANum ANum = do return Refl
    • Relevant bindings include
        geq :: Foo a -> Foo b -> Maybe (a := b)
          (bound at exp-dep-map.hs:20:1)
   |
20 | deriveGEq      ''Foo
   | ^^^^^^^^^^^^^^^^^^^^

Edit: I've continued working on this together with echatav and isovector (GitHub usernames) and we were able to figure this question out further, and we also found that defining GEq and GCompare instances by hand helps. So thank you, @rampion, your answer also corroborates what we've found.

Although it's much less than ideal to define these manually for large record types. I wonder if the TemplateHaskell generators (deriveGCompare, deriveGEq) {would need to be,could be} updated to handle polymorphism.

Also, I've found that for my current use-case the pol'ism I'm looking for is actually closer to

data Foo n a where
  AnInt :: Foo n Int
  AString :: Foo n String
  ANum :: (Num n, Typeable n, Show n) => Foo n n

Hand-defining instances works here too, and again, less than ideal.

instance GEq (Foo n) where
  geq AnInt AnInt = return Refl
  geq AString AString = return Refl
  geq ANum ANum = return Refl
  geq _ _ = Nothing

instance GCompare (Foo n) where
  gcompare AnInt AnInt = GEQ
  gcompare AnInt _ = GLT
  gcompare _ AnInt = GGT
  gcompare AString AString = GEQ
  gcompare AString _ = GLT
  gcompare _ AString = GGT
  gcompare (ANum :: Foo n a) (ANum :: Foo n b) = (eqT @a @b) & \case
    Just (Refl :: a :~: b) -> GEQ
    Nothing   -> error "This shouldn't happen"
  gcompare ANum _ = GLT
  gcompare _ ANum = GGT

Trying to use TH, (e.g. deriveGEq ''Foo or deriveGEq ''(Foo n)) I run into kind-issues.

exp-dep-map.hs:39:1: error:
    • Expecting one more argument to ‘Foo’
      Expected kind ‘* -> *’, but ‘Foo’ has kind ‘* -> * -> *’
    • In the first argument of ‘GEq’, namely ‘Foo’
      In the instance declaration for ‘GEq Foo’
   |
39 | deriveGEq      ''Foo
   | ^^^^^^^^^^^^^^^^^^^^


exp-dep-map.hs:40:19: error: parse error on input ‘Foo’
   |
40 | deriveGEq      ''(Foo n)
   |                   ^^^

Maybe relevant: https://github.com/mokus0/dependent-sum-template/pull/6

Upvotes: 3

Views: 287

Answers (1)

rampion
rampion

Reputation: 89053

The template haskell makes it hard to see what's going on, so I suggest you roll your own instances of GEq to understand the error better.

Look at the definition of GEq:

class GEq f where
  geq :: f a -> f b -> Maybe (a := b)

We don't get any further constraints on a or b, so we'd need to prove (or disprove) type equality on the GADT's constructors alone.

Which the above ANum doesn't give us.

This is fixable, though, if we add another constraint to ANum - Typeable

ANum :: (Num n, Typeable n) => n -> Foo n

Now we can use eqT to witness type equality

geq (ANum _) (ANum _) = eqT

Upvotes: 5

Related Questions