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