Семейство типов типа Хаскелл

В 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, как указано выше?

Ответы

Ответ 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