morteako

{-# LANGUAGE RebindableSyntax #-}

import Prelude hiding ( (>>=),(>>) )
import qualified Prelude as P

(>>) :: Show a => a -> IO () -> IO () 
(>>) x y = print x P.>> y 

end = return ()

morteako

{-@ 
dual1 ::
        f:(a -> a -> a)
    ->  e:a
    ->  assoc : (x:a -> y:a -> z:a -> { f x (f y z) = f (f x y) z } )
    ->  identity : (x:a -> { f x e = x && f e x == x})
    ->  xs:[a]
    ->  { foldr f e xs = foldl f e xs }
@-}
dual1 :: (a -> a -> a) -> a -> (a -> a -> a -> Proof) -> (a -> Proof) -> [a] -> Proof

morteako

import Data.List.Ordered (minus)

figure = 1 : zipWith (+) figure ground

ground = 2 : 4 : minus [5..] figure

morteako

import Data.List (delete)
import Data.List.Ordered (minus)

-- Lazy implementations of Hofstadter Figure-Figure Sequence

--"Straight forward" implementation
lazy1 = go [1..]
    where 
        --putting cur in front of the list instead of using 2 arguments
        go (cur:mem) =  cur : go (cur + m : mem')

morteako

(* exercises : https://gist.github.com/morteako/2dadc9f9b4fff202431513f9475177d6 *)
(* if you find any mistakes, send a mail to morteako@ifi.uio.no *)

(* fn : 'a -> 'a *)
fun id a = a;

(* fn : 'a*'b -> 'a *)
fun first (a,b) = a;

(* fn : 'a*'b -> 'b *)

morteako

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

import           Prelude   hiding (and, pred)

newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }

instance Show Church where
    show (Church c) = show $ c (+1) 0

morteako

Exercise 1

(a)

Write functions with the following type signatures:

fn : 'a -> 'a
fn : 'a*'b -> 'a
fn : 'a*'b -> 'b

morteako

------------------


write the functions with the types:
fn : a -> a
fn : (a*b) -> a
fn : (a*b) -> b


write a function :

morteako

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality

morteako

{-# LANGUAGE RankNTypes #-}

module Main where

import Data.Monoid

newtype Adder = Adder 
    { unAdder :: forall b. Monoid b => Int -> (Int -> b) -> b }