Skip to content

Instantly share code, notes, and snippets.

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 /
Last active January 30, 2017 14:47
Deriving for Classes

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 / OneZero.markdown
Created March 9, 2017 01:53
Musings on One / Zero


data One a = One
  deriving Functor

instance Distributive One where
  distribute :: Functor f => f (One a) -> One (f a)
  distribute _ = One
Icelandjack / or-patterns_as_expressions.markdown
Last active March 19, 2017 12:54
Or-Patterns as Expressions

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

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


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

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 / MultipleInstances.markdown
Created May 27, 2017 16:48
Define multiple instances simultaneously
Icelandjack / irc.log
Created June 1, 2017 15:56
Implication constraints, Show1, Eq1, Read1, Ord1
edwardk, I think I just came up with the most complicated solution to the Show1 problem
Show1 problem?
instance Show (IdentityT m a) where ???
and your solution is?
coming up