読者です 読者をやめる 読者になる 読者になる

Type Family (型族)

Haskell

型族って何?と聞かれたんだけど上手く説明できない.どんなときに便利なの?と聞かれたんだけどそれはHaskell WiKi読めってことで.
で,まぁ無益なプログラムなら,以下のような型だけがあって実体のない(上手い表現を思いつかない)プログラムの例を書ける.
型だけで自然数を定義して,型だけで加法,乗法,べき乗,階乗計算を定義してみました.型族が型の関数であることがわかると思う.この定義では,たとえば,:+: は加法になる.ほんとうに型だけだと,何も見えない「あの世」プログラミングになってしまうので,「浮世(Real World)」プログラミングにするために,Integerという実体のある型の値を使って計算結果を「見える化」してある.

{-# LANGUAGE TypeFamilies
            ,EmptyDataDecls
            ,TypeOperators
            ,FlexibleInstances
            ,OverlappingInstances
            ,UndecidableInstances 
            #-}

module Main where

main :: IO ()
main = print (undefined :: Three :^: Two)

class Nat n where
  toNum :: n -> Integer

instance Nat n => Show n where
  show = show . toNum

data Zero
data Succ n

prev :: Succ n -> n
prev = undefined

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two
type Four  = Two :+: Two

instance Nat Zero where
  toNum = const 0

instance Nat n => Nat (Succ n) where
  toNum = succ . toNum . prev

type family m :+: n :: *
type instance Zero   :+: n = n
type instance Succ m :+: n = Succ (m :+: n)

type family m :*: n :: *
type instance Zero   :*: n = Zero
type instance Succ m :*: n = n :+: (m :*: n)

type family m :^: n :: *
type instance m :^: Zero   = One
type instance m :^: Succ n = m :*: (m :^: n)

type family Fact n :: *
type instance Fact Zero = One
type instance Fact (Succ n) = Succ n :*: Fact n