Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/ind.hs Secret
Last active May 6, 2018

What would you like to do?
{-# 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
= 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 :-)
(<*>) =
(\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) =
(\Nil _ Nil)
(\k (y :- ys) fn head' (fn (Const y)) :- k ys (tail' . fn . Const . getConst))
(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
You can’t perform that action at this time.