Proving halting on computations attached on streams...

computation.hs

{-# LANGUAGE GADTs #-}

-- dependently typing structures that either does halt or doesn't --

class Natural a where
    natural :: a -> a
    natural = id

class Finite a where
    finite :: a -> a
    finite = id

data Zero        = Zero
data Successor n = Successor n
data Infinite    = Infinite

instance Natural  Zero         where { }
instance Natural (Successor n) where { }
instance Natural  Infinite     where { }

instance Finite  Zero         where { }
instance Finite (Successor n) where { }

zero :: Zero
zero = Zero

succ :: (Finite n) => n -> Successor n
succ n = Successor n

data List a length where
    Nil    ::                                       List a  Zero
    Cons   :: (Finite n) => a -> List a n        -> List a (Successor n)
    Stream ::               a -> List a Infinite -> List a  Infinite

instance (Show a) => Show (List a length) where
    show  Nil         = "Nil"
    show (Cons x xs)  = show x ++ " `Cons` " ++ show xs
    show (Stream x _) = show x ++ " `Stream` ..."

from :: Int -> List Int Infinite
from n = Stream n (from (n + 1))

isfinite :: (Finite length) => List a length -> ( )
isfinite _ = ( )

isinfinite :: List a Infinite -> ( )
isinfinite _ = ( )

-- output --
{-

Prelude> :l computation
[1 of 1] Compiling Main             ( computation.hs, interpreted )
Ok, modules loaded: Main.

*Main> isfinite $ Cons 5 $ Cons 7 $ Cons 12 Nil
()

*Main> isinfinite $ Cons 5 $ Cons 7 $ Cons 12 Nil
<interactive>:7:14:
    Couldn't match type ‘Successor (Successor (Successor Zero))’
                  with ‘Infinite’
    Expected type: List a0 Infinite
      Actual type: List a0 (Successor (Successor (Successor Zero)))
    In the second argument of ‘($)’, namely
      ‘Cons 5 $ Cons 7 $ Cons 12 Nil’
    In the expression: isinfinite $ Cons 5 $ Cons 7 $ Cons 12 Nil
    In an equation for ‘it’:
        it = isinfinite $ Cons 5 $ Cons 7 $ Cons 12 Nil

*Main> isinfinite $ from 5
()

*Main> isfinite $ from 5

<interactive>:9:1:
    No instance for (Finite Infinite) arising from a use of ‘isfinite’
    In the expression: isfinite
    In the expression: isfinite $ from 5
    In an equation for ‘it’: it = isfinite $ from 5

*Main> :t Cons 5 $ Cons 9 Nil
Cons 5 $ Cons 9 Nil :: Num a => List a (Successor (Successor Zero))

*Main> :t from 0
from 0 :: Num n => List n Infinite

*Main> Cons 5 $ Cons 9 Nil
5 `Cons` 9 `Cons` Nil

*Main> from 0
0 `Stream` ...

*Main> isinfinite (Cons 5 $ Cons 9 Nil)
<interactive>:19:13:
    Couldn't match type ‘Successor (Successor Zero)’ with ‘Infinite’
    Expected type: List a0 Infinite
      Actual type: List a0 (Successor (Successor Zero))
    In the first argument of ‘isinfinite’, namely
      ‘(Cons 5 $ Cons 9 Nil)’
    In the expression: isinfinite (Cons 5 $ Cons 9 Nil)
    In an equation for ‘it’: it = isinfinite (Cons 5 $ Cons 9 Nil)

*Main> isinfinite (from 0)
()

*Main> isfinite (from 0)
<interactive>:21:1:
    No instance for (Finite Infinite) arising from a use of ‘isfinite’
    In the expression: isfinite (from 0)
    In an equation for ‘it’: it = isfinite (from 0)

*Main> isfinite (Cons 5 $ Cons 9 Nil)
()

*Main> let boom n = n `Cons` boom (n + 1)
<interactive>:26:23:
    Occurs check: cannot construct the infinite type: n ~ Successor n
    Expected type: List a n
      Actual type: List a (Successor n)
    Relevant bindings include
      boom :: a -> List a (Successor n) (bound at <interactive>:26:5)
    In the second argument of ‘Cons’, namely ‘boom (n + 1)’
    In the expression: n `Cons` boom (n + 1)

-}