Skip to content

Instantly share code, notes, and snippets.

@oisdk

oisdk/ind.hs Secret

Last active May 6, 2018 18:46
Show Gist options
  • Save oisdk/23c430b807c788dd43dc4d986c5fdfdd to your computer and use it in GitHub Desktop.
Save oisdk/23c430b807c788dd43dc4d986c5fdfdd to your computer and use it in GitHub Desktop.
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment