日々の流転

λ. 順序数をプログラミング言語の中で実現する

以前に順序数の概念を理解するために書いたコードがあるので、そのときのコードを晒してみます。といっても、当たり前のことを当たり前に書いただけのコードですが。

-- ストリーム
data Stream a = Stream a (Stream a)

instance Functor Stream where
    fmap f (Stream h t) = Stream (f h) (fmap f t)

unfold :: (s -> (a,s)) -> (s -> Stream a)
unfold phi = h
    where h s = case phi s of
                (a,t) -> Stream a (h t)

-- 順序数
data Ordinal
    = OZero
    | OSucc Ordinal
    | OSup (Stream Ordinal)

add :: Ordinal -> Ordinal -> Ordinal
add a OZero     = a
add a (OSucc b) = OSucc (add a b)
add a (OSup b)  = OSup (fmap (add a) b)

mul :: Ordinal -> Ordinal -> Ordinal
mul a OZero     = OZero
mul a (OSucc b) = add (mul a b) a
mul a (OSup b)  = OSup (fmap (mul a) b)

pow :: Ordinal -> Ordinal -> Ordinal
pow a OZero     = OSucc OZero
pow a (OSucc b) = mul (pow a b) a
pow a (OSup b)  = OSup (fmap (pow a) b)

omega :: Ordinal
omega = OSup (unfold (\a -> (a, OSucc a)) OZero)

• OSupの引数のストリームには何らかの正規化のようなことを行うべきだろうか?
• 増大列でない列を排除するのは依存型を使うのが自然だろうけど、GADT等を使ってHaskellで無理やりやる方法はないだろうか?