summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/josef.hs
blob: 3be7dc28dceb5826f27820dac4065e0eb413e4e3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
{-# LANGUAGE GADTs, KindSignatures,
             MultiParamTypeClasses, FunctionalDependencies #-}

-- Program from Josef Svenningsson 

-- Just a short explanation of the program. It contains
-- some class declarations capturing some definitions from
-- category theory. Further down he have a data type for well typed
-- lambda expressions using GADTs. Finally we have a
-- function defining the semantics for lambda terms called
-- 'interp'.

-- Made GHC 6.4 bleat 
--    Quantified type variable `t' is unified with
--        another quantified type variable `terminal'
--    When trying to generalise the type inferred for `interp'


module Bug where

class Category arr where
  idA  :: arr a a
  comp :: arr a b -> arr b c -> arr a c

class Category arr =>
   Terminal terminal arr | arr -> terminal where
  terminal :: arr a terminal

class Category arr =>
      ProductCategory prod arr | arr -> prod  where
  first  :: arr (prod a b) a
  second :: arr (prod a b) b
  pair   :: arr a b -> arr a c -> arr a (prod b c)

class Category arr =>
      CoproductCategory coprod arr | arr -> coprod where
  inLeft  :: arr a (coprod a b)
  inRight :: arr b (coprod a b)
  ccase   :: arr a c -> arr b c -> arr (coprod a b) c

class ProductCategory prod arr => 
      Exponential exp prod arr | arr -> exp where
  eval   :: arr (prod (exp a b) a) b
  curryA :: arr (prod c a) b -> arr c (exp a b)


class (Exponential exp prod arr, Terminal terminal arr) => 
  CartesianClosed terminal exp prod arr | arr -> terminal exp prod 

data V prod env t where
  Z :: V prod (prod env t) t
  S :: V prod env t -> V prod (prod env x) t

data Lambda terminal (exp :: * -> * -> *) prod env t where
    Unit :: Lambda foo exp prod env foo
    Var  :: V prod env t -> Lambda terminal exp prod env t
{-    Lam  :: Lambda terminal exp prod (prod env a) t
	 -> Lambda terminal exp prod env (exp a t)
    App  :: Lambda terminal exp prod env (exp t t') 
	 -> Lambda terminal exp prod env t -> Lambda terminal exp prod env t'
-}

interp :: CartesianClosed terminal exp prod arr => 
	  Lambda terminal exp prod s t -> arr s t
interp (Unit)       = terminal -- Terminal terminal arr => arr a terminal
-- interp (Var Z)      = second
-- interp (Var (S v))  = first `comp` interp (Var v)
-- interp (Lam e)      = curryA (interp e)
-- interp (App e1 e2)  = pair (interp e1) (interp e2) `comp` eval