haskell - Haskell 风格的类型族

Question

在 Haskell 中，我可能会编写一个带有type声明的类型类来创建一个类型族，如下所示：

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 中创建一个类型类约束的类型族，就像上面的那样？

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