Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
module ShapeIndexed where
import Data.Constraint
-- | The type of unary natural numbers (repeated here so the file is
-- self-contained).
data Nat = O | S Nat
-- | A dependent eliminator for @Nat@.
class KnownNat (l :: Nat) where
elimNat :: f 'O -- ^ the 0 case
-> (forall n. KnownNat n => f ('S n)) -- ^ the successor case
-> f l
-- | Instances for the constructors
instance KnownNat 'O where
elimNat f _ = f
instance KnownNat n => KnownNat ('S n) where
elimNat _ f = f
-- | The type of length-indexed vectors.
data Vector (l :: Nat) τ where
Vnil :: Vector O τ
Vcons :: forall l τ. τ -> Vector l τ -> Vector ('S l) τ
instance Functor (Vector l) where
fmap f Vnil = Vnil
fmap f (Vcons x xs) = Vcons (f x) (fmap f xs)
-- | Implementation of @<*>@ for length-indexed vectors.
apVector :: Vector l (α -> β) -> Vector l α -> Vector l β
apVector Vnil Vnil = Vnil
apVector (Vcons f fs) (Vcons x xs) = Vcons (f x) (apVector fs xs)
-- | Implementation of @pure@ for length-indexed vectors.
pureVector :: forall α l. KnownNat l => α -> Vector l α
pureVector a = getPureVector $ elimNat (PureVector Vnil) mkCons
where mkCons :: forall l. KnownNat l => PureVector α ('S l)
mkCons = PureVector $ Vcons a (pureVector a)
-- Local type necessary to get around GHC's lack of type-level lambdas.
newtype PureVector α l = PureVector
{ getPureVector :: Vector l α }
instance KnownNat l => Applicative (Vector l) where
pure = pureVector
(<*>) = apVector
-- | Convert a list into a length-indexed vector.
-- Returns @Nothing@ if the length is not long enough.
fromList :: forall l α. KnownNat l => [α] -> Maybe (Vector l α)
fromList = getFromList $ elimNat (FromList $ const $ Just Vnil) mkCons
where mkCons :: forall l. KnownNat l => FromList α ('S l)
mkCons = FromList $ \ case
[] -> Nothing
(x:xs) -> Vcons x <$> fromList xs
-- Local type to get around GHC's lack of type-level lambdas.
newtype FromList α l = FromList
{ getFromList :: [α] -> Maybe (Vector l α) }
vtail :: Vector ('S l) t -> Vector l t
vtail (Vcons _ xs) = xs
-- | Monadic bind on vectors.
bindVector :: Vector l t -> (t -> Vector l u) -> Vector l u
bindVector Vnil _ = Vnil
bindVector (Vcons x xs) f = case f x of
Vcons z _ -> Vcons z (bindVector xs $ vtail . f)
-- | A @Monad@ instance.
instance KnownNat l => Monad (Vector l) where
return = pure
(>>=) = bindVector
-- | We can learn the structure of a @Nat@ if we have a vector.
learnLength :: Vector l τ -> Dict (KnownNat l)
learnLength Vnil = Dict
learnLength (Vcons _ xs) = case learnLength xs of
Dict -> Dict
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment