10

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 で型クラスに制約のある型ファミリを作成するにはどうすればよいですか?

4

1 に答える 1

8

これの用途が見つかるかどうかはわかりませんが、明らかな翻訳は

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
于 2015-06-03T15:08:02.263 に答える