在 Haskell GADT 中创建递归类型

Question

以下代码为例：

{-# LANGUAGE GADTs #-}

module Example where

data SomeType a where
    MkInt :: Int -> SomeType Int
    MkStr :: String -> SomeType String
    MkRec :: [(String, TypeUnion a)] -> SomeType ???

type TypeUnion a = Either (SomeType Int) (Either (SomeType String) (SomeType ???))

在这个例子中，???应该满足??? = μX. [(String, TypeUnion a)]。因为???的内层的类型参数a和外层的不一样，我觉得用简单的递归解决这个问题是不可行的

不知道有没有办法Haskell可以定义这样的类型？

Answer 1

总是可以使用显式递归：

newtype Fix f = In { out :: f (Fix f) }

现在 Fix SomeType 是 SomeType 的固定点，模显式 wrapping/unwrapping。

在 Haskell GADT 中创建递归类型

Creating recursive type in Haskell GADTs

haskell

programming-languages

type-theory