main = head (Cons (sum (repeat 5 9223372036854775807)) Nil);  --9223372036854775807

-- main = case (bind (fmap (\s . s + 1) (Just 5)) (\s . pure (s + 10))) of {
--     Just a => a ;
--     Nothing => minusOne ;
-- };

---- MAYBE MONAD ----
data Maybe () where {
    Just : Int -> Maybe ()
    Nothing : Maybe ()
};

fmap : (Int -> Int) -> Maybe () -> Maybe () ;
fmap f m = case m of {
    Just a => pure (f a) ;
    Nothing => Nothing ;
};

pure : Int -> Maybe () ;
pure x = Just x;

-- scombinator not working yet :)

bind : Maybe () -> (Int -> Maybe ()) -> Maybe () ;
bind x f = case x of {
    Just x => f x ;
    Nothing => Nothing ;
};

-- represents minus one :)
minusOne : Int ;
minusOne = 9223372036854775807 + 9223372036854775807 + 1;

---- LIST STUFF ----
-- a simple list data type containing ints
data List () where {
    Cons : Int -> List () -> List ()
    Nil  : List ()
};

-- take the length of a list
length : List () -> Int ;
length x = case x of {
    Cons _ xs => 1 + length xs ;
    Nil => 0 ;
};

-- sum a list
sum : List () -> Int ; 
sum x = case x of {
    Cons a xs => a + sum xs ;
    Nil => 0 ;
};

-- sum + length of a list
sumlength: List () -> Int ;
sumlength x = sum x + length x ;

-- take the head of a list
head : List () -> Int ;
head x = case x of {
    Cons h _ => h ;
};

-- repeat an element n times
repeat : Int -> Int -> List () ;
repeat x n = case n of {
    0 => Nil ;
    n => Cons x (repeat x (n + minusOne)) ;
};