spockz

module Main where
data Exp a = Const a
           | Plus (Exp a) (Exp a)
           
type ExpAlgebra a r = (a -> r
                      ,r -> r -> r)

foldExp :: ExpAlgebra a r -> Exp a -> r
foldExp (c, p) = f
  where f (Const a)    = c a

spockz

{-# LANGUAGE GADTs, RankNTypes, ImpredicativeTypes, GeneralizedNewtypeDeriving, KindSignatures #-}

module Main where


data UnitT        = Unit              deriving Show
data Sum aT bT    = Inl aT | Inr bT   deriving Show
data Prod aT bT   = Prod aT bT        deriving Show

data EP bT cT = EP {from :: (bT -> cT), to :: (cT -> bT)}

spockz

data UnitT        = Unit              deriving Show
data Sum aT bT    = Inl aT | Inr bT   deriving Show
data Prod aT bT   = Prod aT bT        deriving Show

data EP bT cT = EP {from :: (bT -> cT), to :: (cT -> bT)}
                    
data Rep tT where
  RUnit  ::                      Rep UnitT
  RInt   ::                      Rep Int
  RChar  ::                      Rep Char 

spockz

{-# LANGUAGE GADTs, RankNTypes, RecordWildCards, ScopedTypeVariables #-}
module Main where

data UnitT        = Unit              deriving Show
data Sum aT bT    = Inl aT | Inr bT   deriving Show
data Prod aT bT   = Prod aT bT        deriving Show

data EP bT cT = EP {from :: (bT -> cT), to :: (cT -> bT)}
                    
data Rep tT where

spockz

 data _≤_ : ℕ → ℕ → Set where
    z≤z : zero ≤ zero
    s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
    z≤s : {n : ℕ} → zero ≤ suc n

  _<=_ : (n : ℕ) → (m : ℕ) → n ≤ m
  _<=_ zero zero       = z≤z
  _<=_ (suc n) (suc m) = s≤s (n <= m)  
  _<=_ zero (suc n)    = z≤s
  _<=_ (suc _) zero = {!?0 : suc .n ≤ zero!}

spockz

  n-suc : (m n : ℕ) → m ≡ n → suc m ≡ suc n
  n-suc p = cong suc p 

>>

/Users/alessandrovermeulen/Documents/Uni/dtp/Assignment1.agda:250,22-23
ℕ !=< (_630 p ≡ _631 p) of type Set
when checking that the expression p has type _630 p ≡ _631 p

spockz

  data _≤2_ : ℕ → ℕ → Set where
    n≤2n :  {m : ℕ} → m ≤2 m
    n≤2s :  {m n : ℕ} → m ≤2 n → m ≤2 suc (n) 

  from-to : {n m : ℕ} {x : n ≤2 m} -> from  (to x) ≡ x
  from-to {.m} {m} {n≤2n} = {!refl!}
  from-to {n} {suc m} {n≤2s y} = cong ({!n≤2s!}) (from-to {n} {m} {y})

>> 
?0 : from (to n≤2n) ≡ n≤2n

spockz

/Users/alessandrovermeulen/Documents/Uni/dtp/Assignment1.agda:294,52-59
Cannot instantiate the metavariable _732 to x ≤2 x since it
contains the variable x which _732 cannot depend on
when checking that the expression n≤2n {x} has type _732 n

spockz

Ass2.lhs:236:13:
    Couldn't match expected type `a1'
           against inferred type `And
                                    True (And (IsBounded (Ins.Var Int Ins.:*: Ins.Rec a)) False)'
      `a1' is a rigid type variable bound by
           the type signature for `gminBound'' at Ass2.lhs:235:33
      NB: `And' is a type function, and may not be injective
    In the expression:
          undefined ::
            IsBounded (Ins.U Ins.:+: ((Ins.Var Int) Ins.:*: (Ins.Rec a)))

spockz

Ass3.lhs:241:40:
    Couldn't match expected type `m1' against inferred type `m'
      `m1' is a rigid type variable bound by
           the polymorphic type
             `forall (m1 :: * -> *). (Alternative m1) => a -> b -> m1 c'
             at Ass3.lhs:241:32
      `m' is a rigid type variable bound by
          the type signature for `zipWithA' at Ass3.lhs:240:25
    In the first argument of `ZipWith', namely `f'
    In the first argument of `frep3', namely `(ZipWith f)'