Arbitrary DFAs with a total delta function

gistfile1.hs

{-# LANGUAGE GADTs, DataKinds, KindSignatures, FlexibleInstances, ScopedTypeVariables #-}

import Test.QuickCheck
import Test.QuickCheck.Gen
import Control.Applicative
import Data.List

-- Peano naturals (used on value and type level)
data Nat = Zero | Suc Nat 

natFromInt :: Int -> Nat
natFromInt 0 = Zero
natFromInt n = Suc (natFromInt $ n - 1)

intFromNat :: Nat -> Int
intFromNat (Zero) = 0
intFromNat (Suc n) = 1 + intFromNat n

-- Type of finite sets of a certain number of elements
data Fin :: Nat -> * where
    FZero :: Fin a
    FSuc  :: Fin a -> Fin (Suc a)
    
natFromFin :: Fin n -> Nat
natFromFin (FZero) = Zero
natFromFin (FSuc n) = Suc $ natFromFin n

-- DFAs, parameterised by the number of states
data DFA n = DFA { delta :: Fin n -> Fin n }

-- Allow us to pull down a natural from type level to value level to inspect it, we can get a singleton of a type-level nat just by calling val.
data Singleton :: Nat -> * where
    SZero :: Singleton Zero
    SSuc  :: Singleton n -> Singleton (Suc n)
    
class Reify (n :: Nat) where
    val :: Singleton n
    
instance Reify Zero where    
    val = SZero

instance Reify n => Reify (Suc n) where
    val = SSuc (val)    

-- Generates a list of all inhabitants of a given type Fin n, used for arbitrary instances. Always invoked as "fin val", which gives us a singleton value
-- to reflect the type.    
fins :: Singleton n -> [Fin n]
fins (SZero) = [FZero]
fins (SSuc n) = FZero : map FSuc (fins n) 

-- Arbitrary natural numbers is straightforward.
instance Arbitrary Nat where
    arbitrary = (arbitrary :: Gen (NonNegative Int)) >>= \(NonNegative x) -> return (natFromInt x)
    shrink (Suc n) = [n]
    shrink Zero    = []

-- Using our fins list, arbitrary numbers in a finite set of a given n is straightforward too:
instance (Reify n) => Arbitrary (Fin n) where
    arbitrary = elements $ fins val

-- Coarbitrary instance of Fin n required for delta function generation:
instance (Reify n) => CoArbitrary (Fin n) where
    coarbitrary = variant . intFromNat . natFromFin

-- We can generate arbitrary DFAs *given* a state space size easily: 
instance (Reify n) => Arbitrary (DFA n) where
    arbitrary = DFA <$> arbitrary

-- Then, we just need to randomly choose a state space size, so we use an existential quantifier to signify that it is unknown at compile-time:  
data Exists :: (Nat -> *) -> * where
    ExI :: (Reify x) => c x -> Exists c
    
-- To convert a nat to a singleton type, we must use exists - Singleton n obviously doesn't work because we don't know what that n will be from
-- compile time checking.
singletonFromNat :: Nat -> Exists Singleton    
singletonFromNat = singletonFromNat' (ExI SZero)
 where singletonFromNat' :: Exists Singleton -> Nat -> Exists Singleton    
       singletonFromNat' acc Zero = acc
       singletonFromNat' (ExI m) (Suc n) = singletonFromNat' (ExI (SSuc m)) n    


natFromSingleton :: Singleton n -> Nat
natFromSingleton (SZero) = Zero
natFromSingleton (SSuc n) = Suc $ natFromSingleton n
       
 
-- Come up with some arbitrary type-level natural
instance Arbitrary (Exists Singleton) where
    arbitrary = singletonFromNat <$> (arbitrary :: Gen Nat) 

-- ... which turns out to be our state space size for generating a totally arbitrary DFA
instance Arbitrary (Exists DFA) where
    arbitrary = (arbitrary :: Gen (Exists Singleton)) 
                  >>= \(ExI (_ :: Singleton n)) -> ExI <$> (arbitrary :: Gen (DFA n)) 
                  

instance Show Nat where
    show x = "n" ++ show (intFromNat x)

instance Show (Fin n) where
    show x = "f" ++ show (intFromNat $ natFromFin x)

instance Show (Singleton n) where
    show n = "s" ++ show (intFromNat (natFromSingleton n))
    
instance Reify n => Show (DFA n) where
    show (DFA d) = "let delta x = case x of {" ++ deltaCases d ++ "} in DFA {- " ++ show (val :: Singleton n) ++ " -} delta" 
       where deltaCases (d :: Fin n -> Fin n) = let fs = fins (val :: Singleton n)
                                            in concat . intersperse "; " $ map (\(a,b) -> show a ++ " -> " ++ show b) $ zip fs $ map d fs
    
instance Show (Exists DFA) where
    show (ExI n) = "ExI (" ++ show n ++ ")"