type families

tyfam.hs

{-# language TypeFamilies, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, DataKinds, TypeOperators, GADTs #-}

module TyFam where

-- A type family is a function on types.
type family Element f

type instance Element [a] = a

instance MonoFunctor [a] where
    monomap = fmap

class MonoFunctor m where
    monomap :: (Element m -> Element m) -> m -> m

-- instance MonoFunctor (Maybe a) where
--     monomap = fmap
--
-- This instance can't resolve the type `Element (Maybe a)`, so it gives
-- the following error:
--
--    Couldn't match type ‘a’ with ‘Element (Maybe a)’
--      ‘a’ is a rigid type variable bound by
--          the instance declaration at tyfam.hs:20:10
--    Expected type: (Element (Maybe a) -> Element (Maybe a))
--                   -> Maybe a -> Maybe a
--      Actual type: (a -> a) -> Maybe a -> Maybe a
--    Relevant bindings include
--      monomap :: (Element (Maybe a) -> Element (Maybe a))
--                 -> Maybe a -> Maybe a
--        (bound at tyfam.hs:21:5)
--    In the expression: fmap
--    In an equation for ‘monomap’: monomap = fmap
--
-- This error is kind of ugly, and if we want to use the type class, and
-- it's *necessary* that we have the type family defined, then we can
-- require that by making it an associated type or by referring to it in
-- the class declaration with a *functional dependency*.

class MonoFunctor' m a | m -> a where
    monomap' :: (a -> a) -> m -> m

-- This requires FlexibleInstances, which is kind of sad.
instance MonoFunctor' [a] a where
    monomap' = fmap

-- The associated type family works nicely, though

class MonoFunctor'' m where
    type Elem m :: *
    monomap'' :: (Elem m -> Elem m) -> m -> m

instance MonoFunctor'' [a] where
    type Elem [a] = a
    monomap'' = fmap

-- These are open type families. A closed type family is where you define
-- all of the instances in one go.

type family IsElem ty xs where
    IsElem ty '[] = 'False
    IsElem ty (ty ': xs) = 'True
    IsElem ty (notTy ': xs) = IsElem ty xs

-- Data families are basically the same thing,  but instead of allowing
-- someone to provide whatever type they want (including doing recursion
-- and other fun stuff), we require that they provide things we can make
-- data constructors out of.

data family FooBar a

data instance FooBar Int = Foo Int | Bar Char

data instance FooBar Char = Wut Char | Lol Int

-- But open data families don't seem super useful to me? The closed
-- equivalent, GADTs, are quite useful though:

data MuhGadt x where
    LInt :: Int -> MuhGadt Int
    LBool :: Bool -> MuhGadt Bool
    IfLol :: MuhGadt Bool -> MuhGadt a -> MuhGadt a -> MuhGadt a

-- You can have an associated data family with a type class, too. The
-- pattern here seems to be a simplification of the following:

class DatabaseToApi db where
    type ApiRep db :: *

    mkModel :: ApiRep db -> db
    mkApiRep :: db -> ApiRep db
    mkKey :: ApiRep db -> Int

data DbUser = DbUser { dbId :: Int, dbName :: String, dbPassword :: String}
data ApiUser = ApiUser { apiId :: Int, apiName :: String }

instance DatabaseToApi DbUser where
    type ApiRep DbUser = ApiUser

    mkModel = undefined
    mkApiRep = undefined
    mkKey = undefined

-- Now, since we generally expect to have these be associated, we may just
-- go ahead and roll them into the class declaration:

class DbToApi db where
    data Api db :: *

instance DbToApi DbUser where
    data Api DbUser = User { lel :: Int, myName :: String }