length-indexed list experiment

Experiment.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import Control.Applicative (Alternative(..))
import Data.Char (isDigit)

newtype Const a b = Const { getConst :: a }
newtype Flip p a b = Flip { runFlip :: p b a }
newtype Compose f g a = Compose { runCompose :: f (g a) }

data Nat = Z | S Nat

type family SUB (n :: Nat) (m :: Nat) :: Nat
type instance SUB n Z = n
type instance SUB (S n) (S m) = SUB n m

class NatInd (n :: Nat) where
  ind :: f Z -> (forall m. NatInd m => f m -> f (S m)) -> f n
instance NatInd Z where
  ind z _f = z
instance (NatInd m) => NatInd (S m) where
  ind z f = f (ind z f)

type ZERO = Z
type ONE = S Z
type TWO = S (S Z)
type THREE = S (S (S Z))
type FOUR = S (S (S (S Z)))
type FIVE = S (S (S (S (S Z))))
type SIX = S (S (S (S (S (S Z)))))
type SEVEN = S (S (S (S (S (S (S Z))))))
type EIGHT = S (S (S (S (S (S (S (S Z)))))))

data EXACTLY (n :: Nat) a where
  NNil :: EXACTLY Z a
  NCons :: a -> EXACTLY n a -> EXACTLY (S n) a
infixr 5 `NCons`

instance Functor (EXACTLY n) where
  fmap f l = case l of
    NNil        -> NNil
    NCons x xs  -> NCons (f x) (fmap f xs)

instance (Show a) => Show (EXACTLY n a) where
  show = show . toListExact

toListExact :: EXACTLY n a -> [a]
toListExact l = case l of
  NNil -> []
  NCons h t -> h : toListExact t

fromListExact :: NatInd n => [a] -> Maybe (EXACTLY n a)
fromListExact = fmap (fmap runFlip . runCompose) . runCompose $ ind z f
  where
    z = Compose $ \l -> Compose $ case l of
      []  -> Just (Flip NNil)
      _   -> Nothing
    f r = Compose $ \l -> Compose $ case l of
      []      -> Nothing
      (x:xs)  -> fmap (Flip . NCons x . runFlip) . runCompose $ runCompose r xs


data UPTO (n :: Nat) a where
  UNil :: UPTO n a
  UCons :: a -> UPTO n a -> UPTO (S n) a
infixr 5 `UCons`

instance Functor (UPTO n) where
  fmap f l = case l of
    UNil        -> UNil
    UCons x xs  -> UCons (f x) (fmap f xs)

instance (Show a) => Show (UPTO n a) where
  show = show . toListUpto

toListUpto :: UPTO n a -> [a]
toListUpto l = case l of
  UNil -> []
  UCons h t -> h : toListUpto t

fromListUpto :: NatInd n => [a] -> Maybe (UPTO n a)
fromListUpto = fmap (fmap runFlip . runCompose) . runCompose $ ind z f
  where
    z = Compose $ \l -> Compose $ case l of
      []  -> Just (Flip UNil)
      _   -> Nothing
    f r = Compose $ \l -> Compose $ case l of
      []      -> Just (Flip UNil)
      (x:xs)  -> fmap (Flip . UCons x . runFlip) . runCompose $ runCompose r xs


{- LIST OF SIZE IN RANGE, REUSING EXACTLY AND UPTO -}

data FROMTO (lo :: Nat) (hi :: Nat) a
  = FROMTO (EXACTLY lo a) (UPTO (SUB hi lo) a)

instance Functor (FROMTO lo hi) where
  fmap f (FROMTO xs ys) = FROMTO (fmap f xs) (fmap f ys)

toListFromto :: FROMTO lo hi a -> [a]
toListFromto (FROMTO xs ys) = toListExact xs <> toListUpto ys

instance Show a => Show (FROMTO lo hi a) where
  show = show . toListFromto

fromListFromto
  :: forall lo hi a. (NatInd lo, NatInd (SUB hi lo))
  => [a] -> Maybe (FROMTO lo hi a)
fromListFromto l =
  let
    i = getConst (ind (Const 0) (Const . (+1) . getConst) :: Const Int lo)
    (l1, l2) = (take i l, drop i l)
  in
    FROMTO <$> fromListExact l1 <*> fromListUpto l2


-- | Lock-step induction over two nats
class NatInd2 (n :: Nat) (m :: Nat) where
  ind2
    :: f Z Z
    -> (forall q. (NatInd2 Z q) => f Z q -> f Z (S q))
    -> (forall p. (NatInd2 p Z) => f p Z -> f (S p) Z)
    -> (forall p q. (NatInd2 p q) => f p q -> f (S p) (S q))
    -> f n m
instance NatInd2 Z Z where
  ind2 zz _zm _nz _nm = zz
instance (NatInd2 Z m) => NatInd2 Z (S m) where
  ind2 zz zm nz nm = zm (ind2 zz zm nz nm)
instance (NatInd2 n Z) => NatInd2 (S n) Z where
  ind2 zz zm nz nm = nz (ind2 zz zm nz nm)
instance (NatInd2 n m) => NatInd2 (S n) (S m) where
  ind2 zz zm nz nm = nm (ind2 zz zm nz nm)


{- LIST OF SIZE IN RANGE, STRUCTURAL -}

data RANGE (lo :: Nat) (hi :: Nat) a where
  RNil :: RANGE Z hi a
  RCons :: a -> RANGE lo hi a -> RANGE (S lo) (S hi) a
  RConsHi :: a -> RANGE lo hi a -> RANGE lo (S hi) a
infixr 5 `RCons`
infixr 5 `RConsHi`

instance Functor (RANGE lo hi) where
  fmap f l = case l of
    RNil          -> RNil
    RCons x xs    -> RCons (f x) (fmap f xs)
    RConsHi x xs  -> RConsHi (f x) (fmap f xs)

instance (Show a) => Show (RANGE lo hi a) where
  show = show . toListRange

toListRange :: RANGE lo hi a -> [a]
toListRange l = case l of
  RNil -> []
  RCons h t -> h : toListRange t
  RConsHi h t -> h : toListRange t

newtype Flip2 p a b c = Flip2 { runFlip2 :: p b c a }
newtype Compose2 f g a b = Compose2 { runCompose2 :: f (g a b) }

fromListRange :: (NatInd2 lo hi) => [a] -> Maybe (RANGE lo hi a)
fromListRange = fmap (fmap runFlip2 . runCompose2) . runCompose2 $ ind2

  -- lo and hi reached zero
  -- if input empty, return empty list
  -- if input non-empty, fail
  ( Compose2 $ \l -> Compose2 $ case l of [] -> Just (Flip2 RNil) ; _ -> Nothing )

  -- lo reached zero
  -- if input empty, return empty list
  -- if input non-empty, recurse
  ( \r -> Compose2 $ \l -> Compose2 $ case l of
          []      -> Just (Flip2 RNil)
          (x:xs)  -> fmap (Flip2 . RConsHi x . runFlip2) . runCompose2 $ runCompose2 r xs )

  -- hi cannot reach zero before lo; fail
  ( \_r -> Compose2 $ \_l -> Compose2 Nothing )

  -- hi and low non-zero
  -- if input empty, fail
  -- if input non-empty, recurse
  ( \r -> Compose2 $ \l -> Compose2 $ case l of
          []      -> Nothing
          (x:xs)  -> fmap (Flip2 . RCons x . runFlip2) . runCompose2 $ runCompose2 r xs )


{- PARSER -}

newtype Parser a = Parser { runParser :: String -> Maybe (a, String) }

parseFailure :: Parser a
parseFailure = Parser $ const Nothing

satisfy :: (Char -> Bool) -> Parser Char
satisfy pred = Parser $ \s -> case s of
  (c:cs) | pred c -> Just (c, cs)
  _ -> Nothing

char :: Char -> Parser Char
char c = satisfy (== c)

digit :: Parser Char
digit = satisfy isDigit

instance Functor Parser where
  fmap f p = Parser $ \s -> case runParser p s of
    Nothing -> Nothing
    Just (a, s') -> Just (f a, s')

instance Applicative Parser where
  pure a = Parser $ \s -> Just (a, s)
  pf <*> pa = Parser $ \s -> case runParser pf s of
    Nothing -> Nothing
    Just (f, s') -> runParser (f <$> pa) s'

instance Alternative Parser where
  empty = parseFailure
  p1 <|> p2 = Parser $ \s -> runParser p1 s <|> runParser p2 s


parseRange :: (NatInd2 lo hi) => Parser a -> Parser (RANGE lo hi a)
parseRange p = fmap runFlip2 . runCompose2 $ ind2
  ( Compose2 . pure . Flip2 $ RNil )

  -- lo reached zero, hi did not.
  -- continue parsing, failure is acceptable
  --
  ( \r -> Compose2 . fmap Flip2 $
            RConsHi <$> p <*> (fmap runFlip2 . runCompose2 $ r)
            <|> pure RNil
  )

  ( \_r -> Compose2 parseFailure )

  -- hi and low non-zero
  -- continue parsing, failure at this level unacceptable
  ( \r -> Compose2 . fmap Flip2 $
            RCons <$> p <*> (fmap runFlip2 . runCompose2 $ r)
  )

I recommend using singletons to implement ind once and for all, rather than using a type class to compute an induction function per natural number.

There should be a function that extracts an EXACTLY from an UPTO: out : UPTO n a -> Sigma Nat (\m -> (m <= n, EXACTLY m a)). That is to say, an UPTO n can be turned into an EXACTLY m for some m <= n.

There should also be a family of functions that 'inject' EXACTLY into UPTO: for a given n : Nat, we should have in_0 : EXACTLY 0 a -> UPTO n a, in_1 : EXACTLY 1 a -> UPTO n a, ..., in_n : EXACTLY n a -> UPTO n a. As a single function this would be in : m <= n -> EXACTLY m a -> UPTO n a.

If you squint, it looks like in takes as arguments the results of out. You could modify in to make this true and you wouldn't lose any precision: in : Sigma Nat (\m -> (m <= n, EXACTLY m a)) -> UPTO n a.

I'm gonna claim that UPTO n a is isomorphic to Sigma Nat (\m -> (m <= n, EXACTLY m a)). So it could be defined as:

data (<=) : Nat -> Nat -> Type where
  LTE_Z : Z <= n
  LTS_S : m <= n -> S m <= S n

data UPTO : Nat -> Type -> Type where
  UPTO : m <= n -> EXACTLY m a -> UPTO n a

The structure of <= is the same as Nat- m <= n actually represents the natural number m.

This means that the new definition of UPTO is a pair of a natural number m (bounded by n), and a list of EXACTLY length m. I think that's a good definition.

Another way of putting it is that UPTO n a is either an EXACTLY 0 a or an EXACTLY 1 a or ... or an EXACTLY n a. It's an iterated sum, which is why I used Sigma.

I think FROMTO can be similarly improved. I'm running out of steam, so I'll just leave this here:

data FROMTO : Nat -> Nat -> Type -> Type where
  FROMTO : lo <= m -> m <= hi -> EXACTLY m a -> FROMTO lo hi a