如何在dependent-map GADT中实现多态值及扩展Foo GADT？

首先，咱们先解决你第一个问题：如何在DMap中存放多态值。DMap的核心逻辑是键（GADT）与值的类型严格绑定——每个键的类型参数a直接决定了对应值的类型f a。要支持多态值，我们可以通过两种实用方式实现：

方式一：用存在类型包装多态值 #

我们可以定义一个存在类型，把任意满足特定约束的值包裹起来，让DMap的值类型指向这个包装器，就能兼容多态场景：

{-# language GADTs #-}
{-# language DeriveGeneric #-}
{-# language DeriveAnyClass #-}
{-# language TemplateHaskell #-}
{-# language StandaloneDeriving #-}
{-# language ExistentialQuantification #-}
import Prelude (Int, String, print, ($), Show)
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(Identity), runIdentity)

-- 定义存在类型，包裹任意可显示的值
data SomeShowable = forall a. Show a => SomeShowable a

-- 补全并扩展原Foo GADT作为DMap的键
data FooKey a where
  FooInt :: FooKey Int
  FooString :: FooKey String
  FooPoly :: FooKey SomeShowable -- 新增多态键

deriveGEq ''FooKey
deriveGCompare ''FooKey

main :: IO ()
main = do
  let myMap = fromList
        [ FooInt ==> Identity 42
        , FooString ==> Identity "hello"
        , FooPoly ==> Identity (SomeShowable [1,2,3]) -- 存放列表
        , FooPoly ==> Identity (SomeShowable 3.14)    -- 存放浮点数
        ]
  print $ runIdentity (myMap ! FooInt)
  print $ runIdentity (myMap ! FooString)
  case runIdentity (myMap ! FooPoly) of
    SomeShowable x -> print x -- 利用Show约束打印多态值

方式二：让GADT键直接携带多态约束 #

另一种更贴合依赖类型风格的方式，是让Foo的构造子本身携带多态约束，这样键就直接声明了对应值的类型约束：

{-# language GADTs #-}
{-# language DeriveGeneric #-}
{-# language DeriveAnyClass #-}
{-# language TemplateHaskell #-}
{-# language StandaloneDeriving #-}
{-# language ConstraintKinds #-}
import Prelude (Int, String, print, ($), Show)
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(Identity), runIdentity)

-- 扩展后的Foo键类型，支持带约束的多态构造子
data FooKey a where
  FooInt :: FooKey Int
  FooString :: FooKey String
  FooShowable :: Show a => FooKey a -- 键本身保证值满足Show约束

-- 注意：带约束的GADT可能需要手动实现GEq/GCompare，模板Haskell生成的实例可能不兼容
instance GEq FooKey where
  geq FooInt FooInt = Just Refl
  geq FooString FooString = Just Refl
  geq (FooShowable :: FooKey a) (FooShowable :: FooKey b) =
    case eqT @a @b of
      Just Refl -> Just Refl
      Nothing -> Nothing
  geq _ _ = Nothing

instance GCompare FooKey where
  gcompare FooInt FooInt = GEQ
  gcompare FooInt _ = GLT
  gcompare _ FooInt = GGT
  gcompare FooString FooString = GEQ
  gcompare FooString _ = GLT
  gcompare _ FooString = GGT
  gcompare (FooShowable :: FooKey a) (FooShowable :: FooKey b) =
    case compare (show (undefined :: a)) (show (undefined :: b)) of
      EQ -> case eqT @a @b of
              Just Refl -> GEQ
              Nothing -> error "Uncomparable showable types"
      ord -> ord

main :: IO ()
main = do
  let myMap = fromList
        [ FooInt ==> Identity 42
        , FooString ==> Identity "world"
        , FooShowable ==> Identity [True, False] -- 布尔列表
        ]
  print $ runIdentity (myMap ! FooInt)
  print $ runIdentity (myMap ! FooShowable)

扩展Foo GADT的实用示例 #

针对你提到的扩展Foo GADT的需求，这里给出一个覆盖多种场景的版本，包括基础类型、自定义类型、多态列表和带约束的构造子：

{-# language GADTs #-}
{-# language DeriveGeneric #-}
{-# language DeriveAnyClass #-}
{-# language TemplateHaskell #-}
{-# language StandaloneDeriving #-}
import Prelude (Int, String, print, ($), Show)
import Data.GADT.Show ()
import Data.GADT.Compare ()
import Data.GADT.Compare.TH (deriveGEq, deriveGCompare)

-- 自定义数据类型，用于演示扩展
data User = User { userName :: String, userAge :: Int } deriving Show

-- 扩展后的Foo GADT
data Foo a where
  -- 原有基础类型构造子
  FooInt :: Int -> Foo Int
  FooString :: String -> Foo String
  -- 新增多态列表构造子
  FooList :: [a] -> Foo [a]
  -- 新增带约束的任意类型构造子
  FooShowable :: Show a => a -> Foo a
  -- 新增自定义数据类型构造子
  FooUser :: User -> Foo User
  -- 新增函数类型构造子（多态函数）
  FooFunc :: (a -> b) -> Foo (a -> b)

-- 生成类型比较实例
deriveGEq ''Foo
deriveGCompare ''Foo

-- 手动实现Show实例，让输出更友好
deriving instance Show (Foo a)

main :: IO ()
main = do
  print $ FooInt 100
  print $ FooString "haskell"
  print $ FooList [1,2,3]
  print $ FooShowable 3.1415
  print $ FooUser (User "Alice" 30)
  print $ FooFunc (+1)

这个扩展后的Foo GADT既支持基础类型，也能处理多态值、自定义类型和函数，完全覆盖了常见的使用场景。

内容的提问来源于stack exchange，提问作者Wizek