``````data Bottom

data (:==:) :: k -> k -> * where
Refl :: a :==: a

type Not p = p -> Bottom

type a :/=: b = Not (a :==: b)
``````

``````data HList (as :: [*]) where
HNil :: HList '[]
HCons :: a -> HList xs -> HList (a ': xs)
``````

## Phantom Type

``````data Circle
data Rectangle

data Shape t where
Circle    :: Float -> Float -> Float -> Shape Circle
Rectangle :: Float -> Float -> Float -> Float -> Shape Rectangle

surface :: Shape t -> Float
surface (Circle _ _ r) = …
surface (Rectangle x1 y1 x2 y2) = …

circum :: Shape Circle -> Float
circum (Circle _ _ r) = …
``````

## Dependent Types

Why use a dependent pair? A part from more advanced uses such as proof construction, online tutorials cite dependent typing as a way to make programs more correct (e.g., avoiding access to zero sized vector). Others say that dependent types allow to describe more precisely the intended behavior of programs. The way I see it is that they can reduce the combinatorial space of cases to consider when building a function.

``````{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies #-}

data N = Z | S N  -- natural numbers

data Vec a (n :: N) where
Nil  :: Vec a Z
Cons :: a -> Vec a n -> Vec a (S n)

vecTail :: Vec a (S n) -> Vec a n
vecTail (Cons _ tl) = tl

data IsNull (n :: N) where
Null    :: IsNull Z
NotNull :: IsNull (S n)

vecNull' :: Vec a n -> IsNull n
vecNull' Nil        = Null
vecNull' (Cons _ _) = NotNull

type family Pred (n :: N) :: N where
Pred Z     = Z
Pred (S n) = n

shorten :: Vec a n -> Vec a (Pred n)
shorten xs = case vecNull' xs of
Null    -> xs
NotNull -> vecTail xs
``````

### Multi-parameter type class

Lucid の例

``````class Term arg result | result -> arg where
termWith :: Text -> [Attribute] -> arg -> result

p_ :: Term arg result => arg -> result
``````

### Type Families

``````-- https://www.youtube.com/watch?v=snOBI8PcbMQ
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy

class Eval x where
eval :: Proxy x -> Int

data One

instance Eval One where
eval _ = 1

instance (Eval a, Eval b) => Eval (Add a b) where
eval _ = eval (Proxy :: Proxy a)
+ eval (Proxy :: Proxy b)

-----------------------------------------

data Hole

class Eval' a where
type Value a r :: *
eval' :: Proxy a -> (Int -> r) -> Value a r

instance Eval' One where
type Value One r = r
eval' _ ret = ret 1

instance (Eval' a, Eval' b) => Eval' (Add a b) where
type Value (Add a b) r = Value a (Value b r)
eval' _ ret = eval' (Proxy :: Proxy a) (\v1 ->
eval' (Proxy :: Proxy b) (\v2 ->
ret (v1 + v2)))

instance Eval' Hole where
type Value Hole r = Int -> r
eval' _ ret n = ret n
``````