真ん中の気持ちです

期待でも諦めでもない真ん中の気持ち。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

data Zero = Zero
data (Nat a) => Succ a = Succ a

class Nat a
instance Nat Zero
instance (Nat a) => Nat (Succ a)

data Vec a n where
    Nil :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)

a ∷ b = Cons a b
infixr 7 ∷

v = 0 ∷ 1 ∷ Nil
n = Nil

type family GetContainerValueType c
type instance GetContainerValueType (Vec a n) = a

class (Nat n) => At n c where
    at :: n -> c -> GetContainerValueType c

-- instance At Zero (Vec a z) where -- 腐った定義
instance (Nat z',Succ z' ~ z) => At Zero (Vec a z) where
    at Zero Nil = error "ゔぁい!!" -- errorに日本語使えませんよ
    at Zero (Cons x xs) = x

instance (Nat i,Nat z',Succ z' ~ z,At i (Vec a z')) => At (Succ i) (Vec a z) where -- まだまだ可愛いクラスコンテキスト
    at (Succ i) Nil = error "ゔぁ〜い!" -- 型が有る限り、ここには来させんよ！！
    at (Succ i) (Cons x xs) = at i xs

{-
instance (Nat i) => At (Succ i) (Vec a z) where
    at (Succ i) Nil = error "hoge"

*Main> at (Succ Zero) n
*** Exception: ?AD!

ポシャって死ぬ

instance (Nat i,Nat z',Succ z' ~ z,At i (Vec a z')) => At (Succ i) (Vec a z) where
だと

*Main> at (Succ Zero) n

<interactive>:1:0:
    Couldn't match expected type `Zero' against inferred type `Succ z''
    When generalising the type(s) for `it'
-}

ここ数日毎日こんな小さいプログラムを幾つも書いてはCoqとAgda2は良いものだと思うわけですね。どれぐらい良いかっていうと、

at : {A : Set0} {n' : Nat} -> (n : Nat) -> Vec A (n + (succ n')) -> A
at zero (cons v _) = v
at (succ n) (cons v r) = at n r

これぐらい。

その他。本当はもっとちゃんとしたものを書くべきだと思うのですが、そういうものは発表資料に入れるわけにも行かないのでほえー。

本当は
http://www.iro.umontreal.ca/~monnier/icfp08.pdf
ぐらいの規模の事をやるべきだと思います。

蒼のエーテルって、どのCDに入ってるんだろう。

マクロスFO.S.T.2 「娘トラ。」

ほほう。

そういえばBoost勉強会に行く時にファミマに行くのであった。

そう！！あとアイマスファミソン8bitは良かった過ぎるのでvol2も買いたい。あるかなー。

なんだろう

文字化けしている。