diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2016
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Author name here nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/TransformeR.cabal b/TransformeR.cabal
new file mode 100644
--- /dev/null
+++ b/TransformeR.cabal
@@ -0,0 +1,61 @@
+Name:                TransformeR
+Version:             0.1.0.0
+Synopsis:            eDSL in R for Safe Variable Transformarion
+Homepage:            https://github.com/remysucre/TransformeR#readme
+License:             BSD3
+License-file:        LICENSE
+Author:              Yisu Remy Wang
+Maintainer:          remywang@protonmail.com
+Copyright:           2016 Yisu Remy Wang
+Category:            DSL, Statistics, Security
+Build-type:          Simple
+-- extra-source-files:
+Cabal-version:       >=1.10
+Description:
+  Arbitrary data transformations that work at the level of single individual data 
+  can be safely applied before applying a differentially private data analysis if 
+  an adversary only gets to observe the result of the differentially private analysis.
+  The current version of the PSI prototype offers support for writing variable 
+  transformations as R programs that can be run on the data before running
+  the other private statistics. Arbitrary R programs can allow for leakage of 
+  information beyond the output, and "side-channel attacks" where an adversary 
+  observes this additional leakage and thereby undermines the privacy guarantees. 
+  
+  TransformeR is a subset of the R language that can serve
+  as a domain specifc language useful to write the needed data transformations and
+  at the same time be more maneageable for preventing security weaknesses
+  and side-channel attacks.
+
+library
+  hs-source-dirs:      src
+  exposed-modules:     Syntax
+                       Types
+                       Parse
+  build-depends:       base >= 4.7 && < 5
+                     , parsec
+                     , mtl
+                     , haskell-src-exts
+  default-language:    Haskell2010
+
+executable TransformeR-exe
+  hs-source-dirs:      app
+  main-is:             Main.hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  build-depends:       base
+                     , TransformeR
+  default-language:    Haskell2010
+
+test-suite TransformeR-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Spec.hs
+--  other-modules:       Trees
+  build-depends:       base
+                     , TransformeR
+                     , QuickCheck
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N 
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/githubuser/TransformeR
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,8 @@
+module Main where
+
+import Syntax
+import Parse
+import Types
+
+main :: IO ()
+main = print "lol"
diff --git a/src/Parse.hs b/src/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Parse.hs
@@ -0,0 +1,103 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RecordWildCards #-}
+module Parse where
+
+import qualified Text.Parsec as P
+import qualified Text.Parsec.Token as PT
+import Text.Parsec.Language
+import Text.Parsec.Expr
+import Text.Parsec ((<?>))
+
+import Control.Applicative
+import Control.Monad.Identity (Identity)
+
+import Syntax
+
+type Parser = P.Parsec String ()
+
+-- | parse olala, calls 'prog'
+parse :: Parser a -> P.SourceName -> String -> Either P.ParseError a
+parse = P.parse 
+
+-- Parser
+
+prog :: Parser Transformation
+prog = do 
+  P.string "transform" 
+  whiteSpace
+  (x, tau1) <- parens $ do x <- identifier
+                           colon
+                           tau1 <- recsig
+                           return (x, tau1)
+  tau2 <- colon *> recsig
+  body <- braces expr
+  return $ TRANS x tau1 tau2 body
+
+expr :: Parser Expression
+expr    = buildExpressionParser table term
+         <?> "expression"
+
+term :: Parser Expression
+term    =  P.try (LIT <$> value)
+       <|> P.try (MUTATE <$> identifier 
+                         <*> brackets identifier 
+                         <*> (P.string ":=" *> expr))
+       <|> REC <$> (braces . commaSep) (do l <- identifier 
+                                           whiteSpace
+                                           P.char '=' 
+                                           whiteSpace
+                                           e <- expr
+                                           return (l, e))
+       <|> P.try (ASSIGN <$> (identifier <* P.string ":=") <*> expr)
+       <|> P.try (OP <$> opr <*> (parens . commaSep) expr)
+       <|> VAR <$> identifier
+       <|> parens expr
+       <?> "expression-term"
+
+value :: Parser Value
+value   =  NUM <$> float
+       <|> CAT <$> stringLiteral
+       <|> MAP <$> (braces . commaSep) (do l <- identifier 
+                                           whiteSpace
+                                           P.char '=' 
+                                           whiteSpace
+                                           v <- value 
+                                           return (l, v))
+       <?> "value"
+
+opr :: Parser OPR
+opr   =  SUM <$ P.char '+'
+     <|> CONCAT <$ P.char '*'
+     <?> "operator"
+
+table :: OperatorTable String u Identity Expression
+table = [ [Postfix (do {f <- brackets identifier; return (\e -> PROJ e f)})]
+        , [binary semi SEQ AssocRight] ]
+
+binary :: P.ParsecT s u m a1 -> (a -> a -> a) -> Assoc -> Operator s u m a
+binary op fun asc = Infix (do{ op ; return fun }) asc
+
+postfix :: P.ParsecT s u m a1 -> (a -> a) -> Operator s u m a
+postfix op fun     = Postfix (do{ op; return fun })
+
+recsig :: Parser Sig
+recsig = Sig <$> (braces . commaSep $ do l <- identifier
+                                         colon
+                                         sig <- tysig
+                                         return (l, sig))
+  
+
+tysig :: Parser Descriptor
+tysig = (uncurry INTERVAL) <$> (P.char 'N' *> brackets (do lb <- float
+                                                           comma
+                                                           ub <- float
+                                                           return (lb, ub)))
+     <|> SET <$> (P.char 'C' *> (brackets . commaSep) stringLiteral)
+     <?> "type signature"
+
+-- Lexer
+
+transformeRDef :: LanguageDef st
+transformeRDef = emptyDef { PT.commentLine = "#"}
+
+PT.TokenParser {..} = PT.makeTokenParser transformeRDef 
diff --git a/src/Syntax.hs b/src/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Syntax.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+module Syntax where
+
+import Data.List
+
+-- ABSTRACT SYNTAX FOR TransformeR
+
+-- A transformation has a name, is signed by a record-type 
+-- and a return-data descriptor and has a body
+-- data Transformation = TRANS Name Sig Sig Body
+data Transformation = TRANS Name Sig Sig Expression
+--  deriving Show
+instance Show Transformation where
+  show (TRANS arg tau1 tau2 e) = 
+    concat [ "transform (", arg, " : ", show tau1, ")\n"
+           , "        : ", show tau2, "\n"
+           , " {", show e, "}"]
+
+-- The body is just a record
+-- type Body = Rec
+
+-- Record-type encodes column names and their descriptors
+data Sig = Sig [(Name, Descriptor)]
+instance Show Sig where
+  show (Sig nds) = 
+    concat [ "{" 
+           ,  concat . (intersperse ", ") $ map (\(n, d) -> n ++ " : " ++ show d) nds
+           , "}"]
+
+-- Severely restricted expressions! 
+-- data Expression =  Name Name -- an exp can be a field access
+--                 | OP OPR [Expression] -- or some simple arithmetics
+--                 | LIT Value -- or a literall
+--   deriving Show
+
+data Expression = LIT Value
+                | PROJ Expression Field
+                | OP OPR [Expression]
+                | REC [(Field, Expression)]
+                | VAR Name
+                | MUTATE Name Field Expression
+                | SEQ Expression Expression
+                | ASSIGN Name Expression
+instance Show Expression where
+  show (LIT v) = show v
+  show (PROJ e f) = concat [show e, "[", f, "]"]
+  -- show (PROJ e f) = "(PROJ " ++ show e ++ show f ++ ")"
+  show (OP opr es) = concat [show opr, "(", (concat . intersperse ", " . map show) es, ")"]
+  show (REC fes) = concat [ "{" 
+                          , (concat . intersperse ", ") (map (\(f, e) -> f ++ " = " ++ show e) fes)
+                          , "}"]
+  show (VAR x) = x
+  show (MUTATE n f e) = concat [n, "[", f, "]:=", show e]
+  show (SEQ e1 e2) = show e1 ++ "; " ++ show e2 
+  show (ASSIGN n e) = n ++ ":=" ++ show e 
+
+type Field = String
+type Rec = [(Name, Expression)]
+-- Descriptor encodes range of data
+type Descriptor = Range
+data Range = INTERVAL Number Number
+           | SET [Name] 
+instance Show Range where
+  show (INTERVAL lb ub) = concat ["N[", show lb, ", ", show ub, "]"]
+  show (SET ns) = concat ["C[", concat $ (intersperse ", ") (map show ns), "]"]
+type Name = String
+data Value = NUM Number 
+           | CAT Category
+           | MAP [(Field, Value)]
+instance Show Value where
+  show (NUM n) = show n
+  show (CAT c) = show c
+  show (MAP fvs) = concat ["{", (concat . intersperse ", ") (map (\(f, v) -> f ++ " = " ++ show v) fvs), "}"]
+
+type Number = Double
+type Category = String
+data OPR = SUM | CONCAT
+instance Show OPR where
+  show SUM = "+"
+  show CONCAT = "*"
diff --git a/src/Types.hs b/src/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Types.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
+
+module Types where
+
+import Syntax
+import Data.List
+import Control.Applicative
+import Debug.Trace
+
+---------------------------
+-- TYPES FOR TransformeR --
+---------------------------
+
+class RefTy t 
+  where tyOK :: t -> Bool
+
+data RecTy = RecTy [(Label, Ty)] -- labeled fields
+  deriving (Show, Eq)
+
+data Ty = NumTy (Number, Number) -- lower and upper bound
+        | CatTy [Category] -- set of catagories
+  deriving (Show, Eq)
+
+type Label = String
+
+type Gamma = [(Name, Either RecTy Ty)] -- type environment
+
+mapsTo g l t = (l, t) : g
+
+---------------------
+-- FORMATION RULES --
+---------------------
+
+instance RefTy Ty
+  where tyOK (NumTy (n1, n2)) = n1 <= n2
+        tyOK (CatTy cs) = isSet cs
+
+instance RefTy RecTy
+  where tyOK (RecTy lts) = all tyOK taus && isSet ls
+          where (ls, taus) = unzip lts
+
+---------------------
+-- SUBTYPING RULES --
+---------------------
+
+instance Ord TransTy
+  where TransTy rtauIn rtauOut <= TransTy rtauIn' rtauOut' 
+          = rtauIn == rtauIn' && rtauOut <= rtauOut'
+
+instance Ord RecTy
+  where RecTy lts <= RecTy lts' 
+          = (length lts == length lts') 
+            && labs == labs'
+            && all id (zipWith (<=) taus taus')
+            where
+              (labs, taus) = unzip lts
+              (labs', taus') = unzip lts'
+
+instance Ord Ty 
+  where NumTy (lb, ub) <= NumTy (lb', ub') = lb' <= lb && ub <= ub'
+        CatTy cs <= CatTy cs' = all (\c -> elem c cs') cs
+
+-------------------------
+-- TYPE SYSTEM/CHECKER --
+-------------------------
+
+data TransTy = TransTy RecTy RecTy 
+  deriving (Show, Eq)
+
+tyTrans :: Transformation -> TransTy
+tyTrans (TRANS arg sigIn sigOut b) 
+  | tyOK tauIn && tyOK tauOut && tau' <= tauOut 
+              = TransTy tauIn tauOut
+  | otherwise = undefined
+  where (Left tau', _) = ty [(arg, Left tauIn)] b
+        tauOut    = tySig sigOut
+        tauIn     = tySig sigIn
+
+readSig :: Sig -> [(Name, Ty)]
+readSig (Sig sig) = map (\(l, s) -> (l, tyDes s)) sig
+  where tyDes (INTERVAL lb ub) = NumTy (lb, ub)
+        tyDes (SET ns) = CatTy ns
+
+tySig :: Sig -> RecTy
+tySig = RecTy . readSig
+
+ty :: Gamma -> Expression -> (Either RecTy Ty, Gamma)
+ty gamma exp =
+  let ty' (PROJ e l) = (Right fTau, gamma')
+        where (rTau, gamma') = ty gamma e
+              Just fTau = lookup l rTauR  
+              Left (RecTy rTauR) = rTau
+      ty' (OP opr es) 
+        | tyOK tauOut = (Right tauOut, gamma')
+        where tauOut = tyJoin opr taus
+              (gamma', taus) = foldl tyNext (gamma, []) es
+              tyNext (g, tau) e = let (t, g) = ty gamma e in (g, t:tau)
+      ty' (LIT (NUM n)) = (Right $ NumTy (n, n), gamma)
+      ty' (LIT (CAT c)) = (Right $ CatTy [c], gamma)
+      ty' (LIT (MAP fvs)) = (ty' . REC) $ map (\(f, v) -> (f, LIT v)) fvs
+      ty' (REC fields) 
+        | tyOK tauRec = (Left tauRec, gamma')
+        | otherwise = undefined
+            where tauRec = RecTy taus
+                  (taus, gamma')          = foldl tyNext ([], gamma) fields
+                  tyNext (taus, g) (l, e) = 
+                      let (Right t, g') = ty g e in (taus ++ [(l,t)], g')
+      ty' (VAR x) = let Just tau = lookup x gamma in (tau, gamma)
+      ty' (MUTATE x l e) = (Left tau', mapsTo gamma' x (Left tau'))
+        where Just (Left (RecTy lts))= lookup x gamma
+              (Right sigma, gamma') = ty' e
+              tau' = if elem l $ map fst lts
+                     then RecTy $ map (\(l', t) -> if l == l' then (l, sigma) else (l, t)) lts
+                     else RecTy $ lts ++ [(l, sigma)]
+      ty' (SEQ e1 e2) = ty gamma' e2 
+        where (_, gamma') = ty' e1
+      ty' (ASSIGN x e) = (t, mapsTo gamma' x t)
+        where (t, gamma') = ty' e
+  in ty' exp
+
+-----------------------------
+-- RULES FOR JOINING TYPES --
+-----------------------------
+
+tyJoin SUM [Right (NumTy (lb1, ub1)), Right (NumTy (lb2, ub2))]
+      | lb1 <= ub1 && lb2 <= ub2 = NumTy (lb1 + lb2, ub1 + ub2)
+      | otherwise = undefined
+tyJoin CONCAT [Right (CatTy cs1), Right (CatTy cs2)]
+      | isSet cs1 && isSet cs2 = CatTy . nub $ cs1 ++ cs2
+      | otherwise = undefined
+tyJoin _ _ = undefined
+
+
+----------------------------
+-- Mother's little helper --
+----------------------------
+
+isSet xs = length xs == length (nub xs)
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,189 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveDataTypeable #-} 
+
+import Syntax
+import Parse
+import Types
+
+import Test.QuickCheck
+import Test.QuickCheck.Arbitrary
+import Control.Applicative
+import Control.Monad
+import Data.Char
+import Data.List
+
+import GHC.Generics
+import Data.Typeable
+
+main = checkTysys
+
+-- checks for tysys
+
+checkTysys :: IO ()
+checkTysys = do
+ fc <- readFile "/home/rem/TransformeR/test/t.R"
+ let res = parse prog "/home/rem/TransformeR/test/t.R" fc
+ case res of 
+   Left e -> putStrLn $ show e
+   Right r -> putStrLn $ show (tyTrans r)
+
+-- checks for parser
+
+checkParse :: IO ()
+checkParse = do
+  quickCheck parseTranOK
+-- fc <- readFile "/home/rem/TransformeR/test/t.R"
+-- let res = parse prog "/home/rem/TransformeR/test/t.R" fc
+-- case res of 
+--   Left e -> putStrLn $ show e
+--   Right r -> putStrLn $ show r
+
+parseTySigOK :: Descriptor -> Bool
+parseTySigOK t = Right t == parse tysig "source" (show t) 
+  
+parseRecSigOK :: Sig -> Bool
+parseRecSigOK r = show r == let Right res = parse recsig "source" (show r) in show res
+
+parseOpOK :: OPR -> Bool
+parseOpOK o = Right o == parse opr "source" (show o)
+
+parseValOK :: Value -> Bool
+parseValOK v = Right v == parse value "source" (show v)
+
+parseExpOK :: Expression -> Bool
+parseExpOK e = show e == let Right res = parse expr "source" (show e) in show res
+
+parseTranOK :: Transformation -> Bool
+parseTranOK t = Right t == parse prog "source" (show t)
+
+eps :: Double
+eps = 0.00001
+
+deriving instance Eq Transformation
+deriving instance Eq Expression
+deriving instance Eq Value
+instance Eq Range where
+  SET xs == SET ys = xs == ys
+  INTERVAL n1 n2 == INTERVAL n3 n4 = 
+    (n1 <= n3 + eps || n1 >= n3 - eps)
+    && (n2 <= n4 + eps || n2 >= n4 - eps)
+deriving instance Eq Sig
+deriving instance Eq OPR
+
+deriving instance Generic Transformation
+deriving instance Generic Expression
+deriving instance Generic Value
+deriving instance Generic Range
+deriving instance Generic Sig
+deriving instance Generic OPR
+
+deriving instance Typeable Transformation
+deriving instance Typeable Expression
+deriving instance Typeable Value
+deriving instance Typeable Range
+deriving instance Typeable Sig
+deriving instance Typeable OPR
+
+-- Default values
+dn = "x"
+dsig = Sig [(dn, ddes)]
+ddes = INTERVAL 1 2
+de = LIT $ NUM 1
+
+arbitraryNum :: Gen Double
+arbitraryNum = elements [1.0, 99.45, 2.34]
+
+arbitraryName = suchThat arbitrary (\s -> (all isEnglish) s && s /= "")
+  where isEnglish x = elem x ['a'..'z']
+
+instance Arbitrary Transformation where
+  arbitrary = TRANS <$> arbitraryName <*> arbitrary <*> arbitrary <*> arbitrary
+  -- shrink = genericShrink
+--  shrink (TRANS n sig1 sig2 e) = [ TRANS dn dsig dsig de
+--                                 , TRANS dn sig1 dsig de
+--                                 , TRANS dn dsig sig2 de
+--                                 , TRANS dn dsig dsig e
+--                                 ]
+  shrink (TRANS n sig1 sig2 e) = [TRANS dn sig1' sig2' e' | (sig1', sig2', e') <- shrink (sig1, sig2, e)]
+
+instance Arbitrary Sig where
+  -- arbitrary = Sig <$> sized (\n -> vectorOf n ((,) <$> arbitraryName <*> arbitrary))
+  arbitrary = Sig <$> vectorOf 3 ((,) <$> arbitraryName <*> arbitrary)
+  shrink = genericShrink
+
+instance Arbitrary Expression where
+  arbitrary = oneof [ LIT <$> arbitrary
+                    , PROJ <$> arbitrary <*> arbitraryName
+                    -- , OP <$> arbitrary <*> sized (\n -> vectorOf n arbitrary)
+                    , OP <$> arbitrary <*> vectorOf 3 arbitrary
+                    , REC <$> vectorOf 3 ((,) <$> arbitraryName <*> arbitrary)
+                    , VAR <$> arbitraryName
+                    , MUTATE <$> arbitraryName <*> arbitraryName <*> arbitrary
+                    , SEQ <$> arbitrary <*> arbitrary
+                    , ASSIGN <$> arbitraryName <*> arbitrary 
+                    ]
+  shrink (LIT x) = []
+  shrink (PROJ e f) = [e]
+  shrink (OP opr [e1, e2, e3]) = [e1, e2, e3]
+  shrink (REC [(f1, e1), (f2, e2), (f3, e3)]) = [e1, e2, e3]
+  shrink (VAR x) = []
+  shrink (MUTATE n l e) = [e]
+  shrink (SEQ e1 e2) = [e1, e2]
+  shrink (ASSIGN n e) = [e]
+
+instance Arbitrary Value where
+  arbitrary = oneof [ NUM <$> arbitraryNum
+                    , CAT <$> arbitraryName
+                    , MAP <$> vectorOf 3 ((,) <$> arbitraryName <*> arbitrary)
+                    ]
+  shrink = genericShrink
+
+instance Arbitrary OPR where
+  arbitrary = elements [SUM, CONCAT]
+  shrink = genericShrink
+
+instance Arbitrary Range where
+  arbitrary = oneof [ INTERVAL <$> arbitraryNum <*> arbitraryNum
+                    -- , SET <$> sized (\n -> vectorOf n arbitraryName)
+                    , SET <$> vectorOf 3 arbitraryName
+                    ]
+  shrink = genericShrink
+
+-- silly checks for parser
+
+-- main = do
+--   fc <- readFile "/home/rem/TransformeR/test/t.R"
+--   let res = parse prog "/home/rem/TransformeR/test/t.R" fc
+--   case res of 
+--     Left e -> putStrLn $ show e
+--     Right r -> putStrLn $ show r
+--   -- (putStrLn . show) <$> res
+-- 
+-- p1 = "transform (y : haha) : yolo { \"a\" }"
+-- 
+-- s = "haha"
+
+-- OLD checks for tysys
+
+-- main :: IO()
+-- main = do 
+--   print $ c1
+--   print $ c2
+--   print $ c3
+--   print $ c4
+--   quickCheck ((\s -> s == s) :: [Char] -> Bool)
+--   quickCheck numberForm
+--   quickCheck catForm
+-- 
+-- numberForm :: Number -> Number -> Bool
+-- numberForm n1 n2 
+--   | n1 <= n2 = tyOK $ NumTy (n1, n2)
+--   | otherwise = not . tyOK $ NumTy (n1, n2)
+-- 
+-- catForm :: [Category] -> Bool
+-- catForm cs
+--   | isSet cs = tyOK $ CatTy cs
+--   | otherwise = not . tyOK $ CatTy cs