データ構築子さんの事・・・分からなく成っちゃった・・・

分からなくなるもなにも、最初から何も知らん！！！！！！！

data Bool :: * where
  true :: Bool
  false :: Bool

みたいな事を書いた時、このtrueとかfalseさんて一体何者なんだろうっていう雰囲気。

例えば、

data Bool :: * where
  true :: Nat
  false :: Nat

これではダメなのか?っていう話がある。Boolなんてクソクラエじゃい！！という。

で、そもそもデータ構築子(上の例だとtrue、false)には実装を書いていないとかっていうのが何とも酷い話だよなーと思っていて。

それから、上の例だと、trueとfalseはBool型の「値」です、って言われて、まぁそうだろうなぁと思うけれども、じゃあ一方で

data Nat :: * where
  zero :: Nat
  succ :: Nat -> Nat

のsuccっていうのは、Natの値なんか?って言われて、うーんていう謎の気持ちになる。

で胡散臭いのが良く分からんて感じで、実装書かなくても良いよーっていう事に対する辻褄合わせとしては多分これは全部Variant/Tagged Disjoint Sum/Tagged Disjoint Unionにぶち込んでるに過ぎないそれなんじゃないだろうか。

だから上の例でtrueとかfalseっていうのは実は、っていうかBoolが実は

Bool は variant {true_ :: Unit,false_ :: Unit} つまり true_ + false_と等しい。

で、
true :: Bool
true = variant { true_ = () } -- ()はUnitの値。
fales :: Bool
false = variant { false_ = ()} -- ()はUnitの値。

みたいに成っていれば、辻褄が多分合う。

Natも同様で

Nat は variant { zero_ :: Unit, succ_ :: Nat} つまり zero_ + succ_と等しい

で、
zero :: Nat
zero = variant { zero_ = () }
succ :: Nat -> Nat
succ n = variant {succ_ = n }

じゃあNat型のListはどうよみたいなのは、Haskellで書くと

data NatList :: * where
  nil :: NatList
  cons :: Nat -> NatList -> NatList

これが

NatList は {nil_ :: Unit, cons_ :: (Nat,NatList) } つまり nil_ + cons_と等しい
ここで(Nat,NatList)はNat型とNatList型のtuple,組

で、
nil :: NatList
nil = variant {nil_ = ()}
cons :: Nat -> NatList -> NatList
cons n nl = variant {cons_ = (n,nl)}

みたいなそれだと良いんじゃないかなーとか。

もちろんvariantさんから値を抜き出す時は、caseとか、まぁ。

でなんでこんな事を考えていたかというと、Agda2では陽に代数データ型を書けるけれども、ITTnにはそんなものはなくて、ITTnにある範疇で考えるとどうなるんだろうなーって事を考えると上みたいな事に。

ITTnにはDisjoint Sumがあるので、その自然な拡張で出来るんだろうなーみたいな事で、なんかなぁ・・・。

というか、HaskellはKindあるんだなーと改めて思ったのでした。

data Hoge :: * -> * where
  hoge :: Nat -> Bool -> Hoge Nat
  foo  :: Nat -> Bool -> Hoge Bool

しかしこれだとなぁ・・・。

Hoge :: * -> *
Hoge = variant {hoge_ :: (Nat,Bool) , foo_ :: (Nat,Bool)}

として

hoge :: Nat -> Bool -> (Hoge,Nat)
hoge n b = (Hoge_,Nat)
  where
    Hoge_ :: Hoge
    Hoge_ = variant {hoge_ = (n,b)}

foo :: Nat -> Bool -> (Hoge,Bool)
foo n b = (Hoge_,Bool)
  where
    Hoge_ :: Hoge
    Hoge_ = variant {foo_ = (n,b)}

胡散臭過ぎる！！

Hogeは型コンストラクタに見えるけど、上の層から見るとデータコンストラクタだし、これもまたVariantで押し込んで

* = {Hoge : *, ...他の型コンストラクタ達 }

とかで良さそうな気も。

あとは

{-
data Hoge : Set0 where
  hoge : (Nat , Bool) -> Hoge
  foo  : (Nat , Bool) -> Hoge

TypeConstHoge : Set0 -> Set0
TypeConstHoge T = Hoge
の方でも

HogeがVariantっぽく素直に書けるし、かつデータコンストラクタの型がカッチリ決まるので
-}

data _+_ (P Q : Set0) : Set0 where -- 結局これが説明出来なくなるとかは無しで！！Variant作れる仮定で
  hoge : P -> P + Q
  foo  : Q -> P + Q

record _,_ (P Q : Set0) : Set0 where
  field
    fst : P
    snd : Q

Hoge : Set0 -> Set0
Hoge T = (Nat , Bool) + (Nat , Bool)

const_hoge : Nat -> Bool -> Hoge Nat
const_hoge n b = hoge (record {fst = zero; snd = true})

const_foo : Nat -> Bool -> Hoge Bool
const_foo n b = foo (record {fst = zero; snd = true})

そもそもこんな回りくどく考えなくても良い気がして来た。

少なくともITTnでは、各型にformation ruleとintroduction ruleとelimination rule、それからequality ruleがあるんだからそれで終わりかなー。

Haskellはまぁ知らなくて、CCだと取りあえず型を定義出来ればコンストラクタの方もゴリ押し出来る気がする。

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}

data Hoge :: * where
  DataConstHoge :: (Int,Bool) -> Hoge
  DataConstFoo  :: (Int,Bool) -> Hoge

type family TypeConstHoge a
type instance TypeConstHoge Int = Hoge
type instance TypeConstHoge Bool = Hoge

hoge :: Int -> Bool -> TypeConstHoge Int
hoge i b = DataConstHoge (i,b)

foo :: Int -> Bool -> TypeConstHoge Bool
foo i b = DataConstFoo (i,b)

-- !!悲しさ
ext :: forall a.TypeConstHoge a -> a
ext (DataConstHoge (i,b)) = i
ext (DataConstFoo  (i,b)) = b
-- !!悲しさ

悲しいお知らせがあります・・・。

悲しいお知らせがあります、はトイレの花子さんで聞いて、そうポンキッキーズで昔やっていたんですけれども、誰か亡くなると、やたら亡くなるんですけれども、校内放送だとかで流れるんですが上の場合だとextが型推論出来ませんよね。

そりゃそうです・・・。そりゃそうですよ・・・。えーとだから。

data Hoge :: * -> * where
  Hoge :: Int -> Bool -> Hoge Int
  Foo  :: Int -> Bool -> Hoge Bool

ext :: forall a.Hoge a -> a
ext (Hoge i b) = i
ext (Foo  i b) = b

これがやりたい。

どうやるにせよ、どうって感じに成る。

あーーーこれ嘘だ。嘘を書いている。Agda2でやってるのは、単に型をそれっぽくしてるだけで、これは酷い。結局データコンストラクタと型が結びついてないので関数ででっち上げただけなので、extをやろうとすると死ぬ。

結局同じコードをHaskellで書き直しただけなので、同様に死んでいる。

まぁでもいいや。