Idriskell

idriskell.hs

{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE InstanceSigs         #-}
{-# LANGUAGE PatternSynonyms      #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns         #-}

import           Data.Type.Equality

import           Prelude            hiding (head, tail, (++))

main :: IO ()
main = pure ()

data Nat
  = Z
  | S Nat
  deriving (Show)

data SNat :: Nat -> * where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

deriving instance Show (SNat x)

(.+.) :: SNat m -> SNat n -> SNat (m + n)
(.+.) SZ SZ     = SZ
(.+.) SZ (SS n) = SS n
(.+.) (SS m) n  = SS $ m .+. n

infixr 5 .+.

(.*.) :: SNat m -> SNat n -> SNat (m ** n)
(.*.) SZ _     = SZ
(.*.) _ SZ     = SZ
(.*.) (SS m) n = gcastWith (mulPlusFact m n) $ (m .*. n) .+. n

infixr 6 .*.

zero = SZ

one = SS SZ

data Fin :: Nat -> * where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n)

type family (m :: Nat) + (n :: Nat) :: Nat where
  Z + n = n
  S m + n = S (m + n)

type family (m :: Nat) ** (n :: Nat) :: Nat where
  m ** Z = Z
  Z ** n = Z
  S m ** n = (m ** n) + n

type family CmpNat (m :: Nat) (n :: Nat) :: Ordering where
  CmpNat Z Z = EQ
  CmpNat Z n = LT
  CmpNat m Z = GT
  CmpNat (S m) (S n) = CmpNat m n

type family Size (t :: *) :: Nat

type instance Size (Vect n a) = n

class Sig (n :: Nat) where
  toSig :: SNat n

instance Sig Z where
  toSig = SZ

instance Sig n => Sig (S n) where
  toSig = SS toSig

type (>) a b = CmpNat a b ~ GT

type (<) a b = CmpNat a b ~ LT

type (==) a b = CmpNat a b ~ EQ

plusZeroRightNeutral :: SNat n -> n + 'Z :~: n
plusZeroRightNeutral SZ     = Refl
plusZeroRightNeutral (SS n) = gcastWith (plusZeroRightNeutral n) Refl

plusSuccFact :: SNat m -> SNat n -> m + 'S n :~: 'S (m + n)
plusSuccFact SZ _     = Refl
plusSuccFact (SS m) n = gcastWith (plusSuccFact m n) Refl

plusAssoc :: SNat m -> SNat n -> SNat o -> m + (n + o) :~: (m + n) + o
plusAssoc SZ _ _     = Refl
plusAssoc (SS m) n o = gcastWith (plusAssoc m n o) Refl

plusCommutes :: SNat m -> SNat n -> m + n :~: n + m
plusCommutes SZ n = gcastWith (plusZeroRightNeutral n) Refl
plusCommutes (SS m) n =
  gcastWith (plusSuccFact n m) $ gcastWith (plusCommutes m n) Refl

mulZeroRightAbsorb :: SNat m -> m ** 'Z :~: 'Z
mulZeroRightAbsorb SZ     = Refl
mulZeroRightAbsorb (SS m) = gcastWith (mulZeroRightAbsorb m) Refl

mulOneLeftNeutral :: SNat n -> 'S 'Z ** n :~: n
mulOneLeftNeutral SZ     = Refl
mulOneLeftNeutral (SS n) = gcastWith (mulOneLeftNeutral n) Refl

mulOneRightNeutral :: SNat n -> n ** 'S 'Z :~: n
mulOneRightNeutral SZ = Refl
mulOneRightNeutral (SS n) =
  gcastWith (plusZeroRightNeutral n) $
  gcastWith (plusSuccFact n SZ) $ gcastWith (mulOneRightNeutral n) Refl

mulPlusFact :: SNat m -> SNat n -> (m ** n) + n :~: ('S m ** n)
mulPlusFact SZ n          = gcastWith (mulOneLeftNeutral n) Refl
mulPlusFact m SZ          = Refl
mulPlusFact (SS m) (SS n) = Refl

mulCommutes :: SNat m -> SNat n -> m ** n :~: n ** m
mulCommutes SZ _ = Refl
mulCommutes _ SZ = Refl
mulCommutes (SS m) (SS n) =
  gcastWith (mulCommutes (m .*. one .+. one) (n .*. one .+. one)) $
  gcastWith (sym $ mulOneRightNeutral (SS n)) $
  gcastWith (sym $ mulOneRightNeutral (SS m)) Refl

mulAssoc :: SNat m -> SNat n -> SNat o -> m ** n ** o :~: m ** (n ** o)
mulAssoc SZ _ _ = Refl
mulAssoc _ SZ _ = Refl
mulAssoc _ _ SZ = Refl
mulAssoc (SS m) (SS n) (SS o) =
  gcastWith
    (mulAssoc (m .*. one .+. one) (n .*. one .+. one) (o .*. one .+. one)) $
  gcastWith (sym $ mulOneRightNeutral (SS o)) $
  gcastWith (sym $ mulOneRightNeutral (SS n)) $
  gcastWith (sym $ mulOneRightNeutral (SS m)) Refl

mulDistributes ::
     SNat m -> SNat n -> SNat o -> (m + n) ** o :~: (m ** o) + (n ** o)
mulDistributes SZ _ _ = Refl
mulDistributes m SZ o =
  gcastWith (plusZeroRightNeutral (m .*. o)) $
  gcastWith (plusZeroRightNeutral m) Refl
mulDistributes _ _ SZ = Refl
mulDistributes (SS m) (SS n) (SS o) =
  gcastWith
    (mulDistributes (m .*. one .+. one) (n .*. one .+. one) (o .*. one .+. one)) $
  gcastWith (sym $ mulOneRightNeutral (SS o)) $
  gcastWith (sym $ mulOneRightNeutral (SS n)) $
  gcastWith (sym $ mulOneRightNeutral (SS m)) Refl

data Vect :: Nat -> * -> * where
  VNil :: Vect 'Z a
  VCons :: a -> Vect n a -> Vect ('S n) a

deriving instance Show a => Show (Vect n a)

class (Size a > 'Z) =>
      Constructable a
  where
  type Head a
  type Tail a
  head :: a -> Head a
  tail :: a -> Tail a
  cons :: Head a -> Tail a -> a
  uncons :: a -> (Head a, Tail a)
  uncons x = (head x, tail x)

instance Constructable (Vect ('S n) a) where
  type Head (Vect ('S n) a) = a
  type Tail (Vect ('S n) a) = Vect n a
  head (VCons x _) = x
  tail (VCons _ xs) = xs
  cons = VCons

pattern (:::) :: Constructable a => Head a -> Tail a -> a

pattern x ::: xs <- (uncons -> (x, xs))
  where x ::: xs = cons x xs

infixr 5 :::

instance Sig n => Functor (Vect n) where
  fmap = vmap toSig

instance Sig n => Applicative (Vect n) where
  pure = vreplicate toSig
  (<*>) = vzipWith toSig ($)

instance Sig n => Monad (Vect n) where
  v >>= f = vjoin toSig $ vmap toSig f v

a :: Vect ('S ('S ('S 'Z))) String
a = "a" ::: "b" ::: "c" ::: VNil

ii = vtake toSig (SS $ SS one) a

aa = a >>= \x -> length x ::: length x * 2 ::: 0 ::: VNil

-- >>> paa
-- VCons 1 (VCons 2 (VCons 0 VNil))
paa = print aa

-- >>> q
-- VCons "b" (VCons "c" (VCons "a" VNil))
q = print $ vshift (SS one) toSig a

-- >>> m
-- VCons 1 (VCons 2 (VCons 3 VNil))
m = const 1 ::: const 2 ::: const 3 ::: VNil <*> a

b = head a

c = tail a

-- >>> d
-- "c"
d = vindex toSig (FS $ FS FZ) a

e = vappend toSig toSig a a

o = f a

-- >>> g
-- "b"
g = print o

f (x ::: (y ::: (z ::: xs))) = y

vjoin :: SNat n -> Vect n (Vect n a) -> Vect n a
vjoin SZ _              = VNil
vjoin (SS n) (x ::: xs) = head x ::: vjoin n (vmap n tail xs)

vshift :: Show a => SNat m -> SNat n -> Vect ('S n) a -> Vect ('S n) a
vshift SZ _ v = v
vshift (SS m) n v =
  let (i, l) = (vinit n v, vlast n v)
   in vshift m n $ vappend one n (pure l) i

vreplicate :: SNat n -> a -> Vect n a
vreplicate SZ _     = VNil
vreplicate (SS n) x = x ::: vreplicate n x

vinit :: SNat n -> Vect ('S n) a -> Vect n a
vinit SZ _              = VNil
vinit (SS n) (x ::: xs) = x ::: vinit n xs

vtake :: SNat m -> SNat n -> Vect (n + m) a -> Vect n a
vtake _ SZ _              = VNil
vtake m (SS n) (x ::: xs) = x ::: vtake m n xs

vlast :: SNat n -> Vect ('S n) a -> a
vlast SZ (x ::: _)      = x
vlast (SS n) (_ ::: xs) = vlast n xs

vindex :: SNat n -> Fin ('S n) -> Vect ('S n) a -> a
vindex _ FZ (x ::: _)           = x
vindex (SS n) (FS k) (_ ::: xs) = vindex n k xs

vzip :: SNat n -> Vect n a -> Vect n b -> Vect n (a, b)
vzip n = vzipWith n (,)

vzipWith :: SNat n -> (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vzipWith SZ _ _ _                       = VNil
vzipWith (SS n) f (x ::: xs) (y ::: ys) = f x y ::: vzipWith n f xs ys

vappend :: SNat m -> SNat n -> Vect m a -> Vect n a -> Vect (m + n) a
vappend n SZ u _              = gcastWith (plusZeroRightNeutral n) u
vappend SZ _ _ v              = v
vappend (SS n) m (x ::: xs) v = x ::: vappend n m xs v

vmap :: SNat n -> (a -> b) -> Vect n a -> Vect n b
vmap SZ _ _              = VNil
vmap (SS n) f (x ::: xs) = f x ::: vmap n f xs