Skip to content

Instantly share code, notes, and snippets.

View gist:660ccce86d4461fd467638368f0d1ac2

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
Icelandjack / DerivingClasses.md
Last active Jan 30, 2017
Deriving for Classes
View DerivingClasses.md

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

View OneZero.markdown

Representable

data One a = One
  deriving Functor

instance Distributive One where
  distribute :: Functor f => f (One a) -> One (f a)
  distribute _ = One
View or-patterns_as_expressions.markdown
View Deriving.markdown

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
Icelandjack / 11439.markdown
Created May 17, 2017
GHC Trac #11439 (case signatures?)
View 11439.markdown

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

View Eq.markdown

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
Icelandjack / Methods.markdown
Created May 27, 2017
Type Family for Type Class Methods
View Methods.markdown

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
Icelandjack / MultipleInstances.markdown
Created May 27, 2017
Define multiple instances simultaneously
View MultipleInstances.markdown
@Icelandjack
Icelandjack / irc.log
Created Jun 1, 2017
Implication constraints, Show1, Eq1, Read1, Ord1
View irc.log
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