Haskell-style type families

10
votes

In Haskell, I might write a typeclass with a type declaration to create a type family, like so:

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

And then write instances like this:

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

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

I'm aware that you can create typeclasses and type-level functions in Idris, but the methods operate on data of the given type, not the type itself.

How can I make a typeclass-constrained type family in Idris like the one above?

1
haskelltype-familiesidris
I think you don't need this - remember you have even better tools: first class types - so you can write Elem as a function – Random Dev
@Carsten I realise that, but how might I constrain that function to instances of that typeclass? – AJF
I think you probably don't have a problem with associated type families at all. Idris does not, however, offer associated data families, and I don't know if that will keep you from doing something or other. It also doesn't have Haskell-style non-associated type families; there is no pattern matching whatsoever on type constructors. – dfeuer

1 Answers

8
votes

I have no clue if you will ever find a use for this, but I think the obvious translation should be

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

usage

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