Haskell风格的类型族

Question

在Haskell中，我可能会编写一个类型类(typeclass)，并使用type声明来创建一个类型族(type family)，代码如下：

class ListLike k where
    type Elem ::  * -> *
    fromList :: [Elem k] -> k

然后像这样编写实例：

instance ListLike [a] where
    type Elem [a] = a
    fromList = id

instance ListLike Bytestring where
    type Elem Bytestring = Char
    fromList = pack

我知道在 Idris 中可以创建类型类和类型级函数，但这些方法是针对给定类型的数据而非类型本身操作的。

我该如何像上面那样在 Idris 中创建一个受类型类限制的类型族？

- AJF

---

我认为你不需要这个 - 记住你有更好的工具：一等类型 - 所以你可以将Elem写成一个函数。 - Random Dev

@Carsten 我明白，但我该如何将该函数限制为该类型类的实例？ - AJF

我认为你可能完全没有与相关联类型族的问题。不过，Idris并没有提供相关联的数据族，而我不知道这是否会阻止你做某些事情。它也没有Haskell风格的非相关联类型族；在类型构造函数上根本没有模式匹配。 - dfeuer

Answer 1

我不知道你是否会有机会用到这个，但我认为显而易见的翻译应该是：

class ListLike k where
    llElem : Type
    fromList : List llElem -> k

instance ListLike (List a) where
    llElem = a
    fromList = id

instance ListLike (Maybe a) where
  llElem = a
  fromList [] = Nothing
  fromList (a::_) = Just a

使用

λΠ> the (Maybe Int) (fromList [3])
Just 3 : Maybe Int
λΠ> the (List Int) (fromList [3])
[3] : List Int

- Random Dev

---

我可能会问，为什么不是 llElem : Type -> Type 而是 Type ？这肯定是一个无法判定的实例吧？ - AJF

将其加载到idris中并查看类型（:t）-您可以在家族内使用data而不是type几乎可以获得相同的Haskell- llElem是ListLike k => Type，因此在ListLike k => List llElem -> k中是有意义的，您在这里不需要/不想要更多（或者我猜是这样）。 - Random Dev

在Haskell中另一种方法是使用两个参数类型类和函数依赖 - 重要的事实是k意味着llElem。 - Random Dev

@AJFarmar llElem 不能单独使用，但可以通过使用 fromList 来确定适当的实例。目前在此类的定义中，Idris 实际上并没有检查这一点（但它应该很快会检查）。 - Edwin Brady

对我来说，Idris 0.9.18针对给定代码报告了3个错误： DecEq.idr:1:7:在展开Main.fromList的类型时： 无法解析类型类ListLike k DecEq.idr:5:10:ListLike不是一个类型类 DecEq.idr:9:10:ListLike不是一个类型类 - Boldizsár Németh