Icelandjack

Reddit discussion.

Disclaimer 1: Type classes are great but they are not the right tool for every job. Enjoy some balance and balance to your balance.

Disclaimer 2: I should tidy this up but probably won’t.

Disclaimer 3: Yeah called it, better to be realistic.

Type classes are a language of their own, this is an attempt to document features and give a name to them.

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

Are these examples of

• Ticket #12369
• Ticket #12766

Application

data App0 :: Type -> Type where
  App0 :: a -> App0

Icelandjack

Nested

Showing where types change:

infixr 5 :::
data Nest a = N | a ::: Nest (a, a)

In

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

HList : Sublist -> Hask

type Cat k = k -> k -> Type

data Sublist :: Cat [a] where
  Stop :: Sublist '[] '[]
  Drop :: Sublist xs ys -> Sublist (x:xs) ys
  Keep :: Sublist xs ys -> Sublist (x:xs) (x:ys)

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

wip, spin-off gists: https://gist.github.com/Icelandjack/e42495341f6029aad8c7e4e4a12c34ce

Monad gives Applicative, Applicative etc. gives Num, Floating, Fractional (regardless of actual subclass relationship)

Setting it up

WrapMonad tells us that a Monad implies Functor, Applicative

instance Monad m => Functor     (WrappedMonad m)