fork(1) download

copy

{-# LANGUAGE FunctionalDependencies, 
             MultiParamTypeClasses, 
             FlexibleInstances,
             FlexibleContexts,
             UndecidableInstances,
             ScopedTypeVariables,
             OverlappingInstances,
             GADTs #-}
 
import Prelude hiding (succ)
 
data Null
data Succ a
 
type One = Succ Null
type Two = Succ One
type Three = Succ Two
 
newtype SafeList l a = SafeList [a]
 
nil :: SafeList Null a
nil = SafeList []
cons :: a -> SafeList n a -> SafeList (Succ n) a
cons a (SafeList x) = SafeList $ a:x
 
at :: (Less i n) => SafeList n a -> LessThanT i Int -> a
at (SafeList a) = (a!!) . unpack
 
-- a < b
class Less a b where
instance Less Null (Succ a)
instance (Less a b) => Less (Succ a) (Succ b)
 
newtype LessThanT a b = LessThan b deriving (Show)
instance Less (LessThanT a b) a
unpack (LessThan x) = x
 
class Plus a b c | a b -> c where
instance (Num a) => Plus Null a a
instance Plus a Null a
instance (Plus a b c) => Plus (Succ a) (Succ b) c
 
class ToLess a b where
  less :: a -> Maybe (LessThanT b a)
 
-- Shifting values to the type level isn't fast yet possible
instance (Num a, Eq a) => ToLess a One where
  less 0 = Just (LessThan 0)
  less _ = Nothing
 
instance (Num a, Eq a, ToLess a b) => ToLess a (Succ b) where
  less n = case (less $ n - 1) :: Maybe (LessThanT b a) of
             Nothing -> Nothing
             Just _  -> Just (LessThan n)
 
succ :: (Num x) => LessThanT a x -> LessThanT (Succ a) x
succ (LessThan n) = LessThan $ n + 1
 
getAt' :: (i' ~ Succ i, Less i' n) => SafeList n a -> LessThanT i Int -> a
getAt' a i = at a $ succ i
 
main = do
  m <- readLn :: IO Int
  n <- readLn :: IO Int
  print $ foldl cons nil [1..n]
 

[1 of 1] Compiling Main             ( prog.hs, prog.o )

prog.hs:65:17:
    Couldn't match type `Succ n0' with `Null'
    Expected type: SafeList Null a0
                   -> SafeList n0 (SafeList Null a0) -> SafeList Null a0
      Actual type: SafeList Null a0
                   -> SafeList n0 (SafeList Null a0)
                   -> SafeList (Succ n0) (SafeList Null a0)
    In the first argument of `foldl', namely `cons'
    In the second argument of `($)', namely `foldl cons nil [1 .. n]'
    In a stmt of a 'do' block: print $ foldl cons nil [1 .. n]

prog.hs:65:30:
    Couldn't match expected type `SafeList n0 (SafeList Null a0)'
                with actual type `Int'
    In the expression: n
    In the third argument of `foldl', namely `[1 .. n]'
    In the second argument of `($)', namely `foldl cons nil [1 .. n]'

Standard output is empty