{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

import Prelude hiding (fst, snd)

-- 型, 関数fst, sndの3つ組. ペアだけど3つ組で構成される.
class Pair p a b | p -> a, p -> b where
  fst :: p -> a
  snd :: p -> b

-- ペアの例1
instance Pair (a, b) a b where
  fst (a, _) = a
  snd (_, b) = b

-- ペアの例2.
-- 3つの要素を持つTupleでも, ペアを実装することができる
--                           <=> ペアの要件を満たすことができる
instance Pair (a, b, c) a b where
  fst (a, _, _) = a
  snd (_, b, _) = b

-- ペアの例3.
-- ペアを実装する自作の構造.
data Tup2 a b = Tup2 a b

instance Pair (Tup2 a b) a b where
  fst (Tup2 a _) = a
  snd (Tup2 _ b) = b

-- ペアに普遍射(x, univ)を持つ条件を課せば, それは積と呼べる
-- 積とは, 任意のペアから一意の射が伸びるようなペアのこと
-- どんなペアからも関数univを使って得られるようなペアを, 積と呼ぶ
class Pair x a b => Product x a b where
  univ :: Pair y a b => y -> x

-- 積の例1
instance Product (a, b) a b where
  univ y = (fst y, snd y)

-- (a, b, c)はペアであるが積ではない
-- 3つ目の要素cを得られず, univを実装できない

-- 積の例2
instance Product (Tup2 a b) a b where
  univ y = Tup2 (fst y) (snd y)

-- 積は, どのようなペアからもunivを使って得られるようなペア
-- すなわち, 任意の積から任意の積への関数univは, 常に同型射である
--           <=> 任意の積は, 互いに同型である
-- 積は同型を除いて一意
iso :: (Product p a b, Product q a b) => p -> q
iso = univ

main :: IO ()
main = pure ()