ind.hs

{-# language RankNTypes             #-}
{-# language DataKinds              #-}
{-# language GADTs                  #-}
{-# language TypeFamilies           #-}
{-# language TypeFamilyDependencies #-}
{-# language UnicodeSyntax          #-}
{-# language TypeOperators          #-}
{-# language ScopedTypeVariables    #-}
{-# language PolyKinds              #-}

{-# options_ghc -Wall #-}
{-# options_ghc -fno-warn-unticked-promoted-constructors #-}

module Induction where

import Data.Kind
import Data.Functor.Const

data ℕ
    = Z
    | S ℕ

type family (t ∷ k) ∝ (n ∷ ℕ) = (a ∷ Type) | a → t n k

class Finite n where
    induction ∷ t ∝ Z → (∀ k. t ∝ k → t ∝ S k) → t ∝ n

instance Finite Z where
    induction z _ = z
    {-# inline induction #-}

instance Finite n ⇒ Finite (S n) where
    induction z s = s (induction z s)
    {-# inline induction #-}

infixr 5 :-
data List n a where
        Nil  ∷ List Z a
        (:-) ∷ a → List n a → List (S n) a

type instance '(List,a) ∝ n = List n a

instance Functor (List n) where
    fmap _ Nil = Nil
    fmap f (x :- xs) = f x :- fmap f xs

data a ↦ b
type instance ((x ∷ a) ↦ (y ∷ b)) ∝ n = (x ∝ n) → (y ∝ n)

instance Finite n ⇒
         Applicative (List n) where
    pure x = induction Nil (x :-)
    (<*>) =
        induction
            (\Nil Nil → Nil)
            (\k (f :- fs) (x :- xs) → f x :- k fs xs)

type instance (Const a ∷ ℕ → Type) ∝ n = Const a n

head' ∷ List (S n) a → a
head' (x :- _) = x

tail' ∷ List (S n) a → List n a
tail' (_ :- xs) = xs

instance Finite n ⇒
         Monad (List n) where
    xs >>= (f ∷ a → List n b) =
        induction
            (\Nil _ → Nil)
            (\k (y :- ys) fn → head' (fn (Const y)) :- k ys (tail' . fn . Const . getConst))
            xs
            (f . getConst ∷ Const a n → List n b)