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)

出典: DataKinds 言語拡張を使って Typed Heterogeneous List とその基本操作を実装してみた

Constraint

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) = …

https://www.reddit.com/r/haskell/comments/2jsz4t/function_on_a_single_member_of_a_sum_type/clevra9

存在型

Reflection

Type Inference

Parametricity

定理証明

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.
Vittorio Zaccaria - Home page

{-# 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

出展: Smarter conditionals with dependent types: a quick case study

一般化代数的データ型

Multi-parameter type class

Lucid の例

class Term arg result | result -> arg where
  termWith :: Text -> [Attribute] -> arg -> result
-- https://hackage.haskell.org/package/lucid/docs/Lucid-Base.html#t:Term

p_ :: Term arg result => arg -> result
-- https://hackage.haskell.org/package/lucid/docs/Lucid-Html5.html#v:p_

Functional dependencies

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
data Add a b

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

Singleton

カインド