Icelandjack

Total Type Families

A total type family feels quite comfortable. By total here, I mean a type family whose equations cover all the possible cases and which is guaranteed to terminate. That is, a total type family is properly a function on types. Those other dependently typed languages have functions on types, and they seem to work nicely. I am completely unbothered by total type families.

— What are type families?

Non-covering Type Families (are strange)

A non-covering type family is a type family whose patterns do not cover the whole space.

Icelandjack

Just like you can derive instances for data types (example is from homoiconic)

data Foo = F Int Bool 
 deriving Show

maybe it makes sense to do it for certain type classes.

If you define

Icelandjack

Representable

data One a = One
  deriving Functor

instance Distributive One where
  distribute :: Functor f => f (One a) -> One (f a)
  distribute _ = One

Icelandjack

This plays with an interesting idea from Pattern synonyms, arbitrary patterns as expressions, brought up in the ghc-proposal for or-patterns.

data Exp
  = Val Int 
  | Add Exp Exp
  | Mul Exp Exp
  | Div Exp Exp

Icelandjack

One of the best parts of Haskell is getting functionality for free

newtype T a = T_ (Compose [] Maybe a) 
  deriving (Functor, Foldable, Traversable, Applicative, Alternative)

{-# Complete T #-}
pattern T :: [Maybe a] -> T a
pattern T a = T_ (Compose a)

Icelandjack

Good example from Eisenberg:

type Effect = Type -> Type -> Type -> Type

class Handler (e :: Effect) (m :: Type -> Type) where
  handle :: e res res' t -> res -> (res' -> t -> m a) -> m a  

For Random

Icelandjack

1

Comparing IO a for equality, cannot be captured by Bool.

class EQ a where
  type Logic a
  (=~=) :: a -> a -> Logic a 
  
instance EQ Int where

Icelandjack

This could be synthesised

type family   Methods (cls :: Type -> Constraint) (a :: Type) = (res :: [Pair Symbol Type]) | res -> a
type instance Methods A a = '["a" :- a]
type instance Methods B b = '["b" :- (b -> b)]
type instance Methods C c = '["c" :- (c -> Int), "b" :- (c -> c), "a" :- c]

data Pair a b = a :- b
 

Icelandjack

Idea from https://gist.github.com/Icelandjack/e1ddefb0d5a79617a81ee98c49fbbdc4

Works great for concrete types

data A = MkA

instance (Eq & Ord & Show & Arbitrary) A where
  (==) :: A -> A -> Bool
 MkA == MkA = True

Icelandjack

mniip
edwardk, I think I just came up with the most complicated solution to the Show1 problem 
phadej
Show1 problem? 
mniip
instance Show (IdentityT m a) where ??? 
phadej
and your solution is? 
mniip
coming up