diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.18
 name: language-ats
-version: 1.2.0.10
+version: 1.2.0.11
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -240,6 +240,7 @@
     <0> "addr@"                  { tok (\p _ -> alex $ Keyword p KwAddrAt) }
     <0> "view@"                  { tok (\p _ -> alex $ Keyword p KwViewAt) }
     <0> sta                      { tok (\p _ -> alex $ Keyword p KwSta) }
+    <0> as                       { tok (\p _ -> alex $ Keyword p KwAs) }
     <0> symintr                  { tok (\p _ -> alex $ Keyword p KwSymintr) }
     <0> absview                  { tok (\p _ -> alex $ Keyword p KwAbsview) }
     <0> exception                { tok (\p _ -> alex $ Keyword p KwException) }
@@ -393,6 +394,7 @@
              | KwAddrAt
              | KwAddr
              | KwSta
+             | KwAs
              | KwViewAt
              | KwViewdef
              | KwSymintr
@@ -511,6 +513,7 @@
     pretty KwAddrAt = "addr@"
     pretty KwAddr = "addr"
     pretty KwSta = "sta"
+    pretty KwAs = "as"
     pretty KwStacst = "stacst"
     pretty KwViewAt = "view@"
     pretty KwViewdef = "viewdef"
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -128,6 +128,7 @@
     viewPlusMinus { Keyword _ (KwView $$) }
     raise { Keyword $$ KwRaise }
     tkindef { Keyword $$ KwTKind }
+    as { Keyword $$ KwAs }
     assume { Keyword $$ KwAssume }
     addrAt { Keyword $$ KwAddrAt }
     viewAt { Keyword $$ KwViewAt }
@@ -341,6 +342,7 @@
         | at Pattern { AtPattern $1 $2 }
         | identifier Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
         | identifierSpace Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
+        | Pattern as Pattern { As $2 $1 $3 }
         | Existential Pattern { ExistentialPattern $1 $2 }
         | minus {% left $ Expected $1 "Pattern" "-" }
         | plus {% left $ Expected $1 "Pattern" "+" }
@@ -513,6 +515,7 @@
      | vtype { VType (token_posn $1) (get_addendum $1) }
      | openParen Sort comma Sort closeParen { TupleSort $1 $2 $4 }
      | doubleParens { NamedSort "()" }
+     | Sort mutateArrow Sort { ArrowSort $2 $1 $3 }
      | IdentifierOr { NamedSort $1 }
      | IdentifierOr plus { NamedSort ($1 <> "+") }
 
@@ -907,10 +910,8 @@
             | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) }
             | overload lsqbracket rsqbracket with identifierSpace of intLit { OverloadIdent $1 "[]" (Unqualified $ to_string $5) (Just $7) }
             | overload dot identifierSpace with Name { OverloadIdent $1 ('.' : (to_string $3)) $5 Nothing }
-            | assume identifierSpace eq Type { Assume (Unqualified (to_string $2)) [NoArgs] $4 }
-            | assume Name eq Type { Assume $2 [NoArgs] $4 }
-            | assume Name doubleParens eq Type { Assume $2 [] $5 }
-            | assume Name openParen Args closeParen eq Type { Assume $2 $4 $7 }
+            | assume identifierSpace SortArgs eq Type { Assume (Unqualified (to_string $2)) $3 $5 }
+            | assume Name SortArgs eq Type { Assume $2 $3 $5 }
             | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 }
             | TypeDecl { $1 }
             | symintr Names { SymIntr $1 $2 }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -14,6 +14,7 @@
                                 ) where
 
 import           Control.Composition          hiding ((&))
+import           Data.Bool                    (bool)
 import           Data.Functor.Foldable        (cata)
 import           Language.ATS.Types
 import           Lens.Micro
@@ -214,6 +215,7 @@
         a (AtPatternF _ p)             = "@" <> p
         a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p
         a (ExistentialPatternF e p)    = pretty e <> p
+        a (AsF _ p p')                 = p <+> "as" <+> p'
 
 argHelper :: Eq a => (Doc -> Doc -> Doc) -> Arg a -> Doc
 argHelper _ (Arg (First s))   = pretty s
@@ -257,13 +259,15 @@
         a (SCaseF ad e sls) = "case" <> pretty ad <+> e <+> "of" <$> indent 2 (prettyCases sls)
 
 instance Eq a => Pretty (Sort a) where
-    pretty (T0p ad)           = "t@ype" <> pretty ad
-    pretty (Vt0p ad)          = "vt@ype" <> pretty ad
-    pretty (NamedSort s)      = text s
-    pretty Addr               = "addr"
-    pretty (View _ t)         = "view" <> pretty t
-    pretty (VType _ a)        = "vtype" <> pretty a
-    pretty (TupleSort _ s s') = parens (pretty s <> "," <+> pretty s')
+    pretty = cata a where
+        a (T0pF ad)           = "t@ype" <> pretty ad
+        a (Vt0pF ad)          = "vt@ype" <> pretty ad
+        a (NamedSortF s)      = text s
+        a AddrF               = "addr"
+        a (ViewF _ t)         = "view" <> pretty t
+        a (VTypeF _ a')       = "vtype" <> pretty a'
+        a (TupleSortF _ s s') = parens (s <> "," <+> s')
+        a (ArrowSortF _ s s') = s <+> "->" <+> s'
 
 instance Eq a => Pretty (Type a) where
     pretty = cata a where
@@ -584,8 +588,7 @@
     pretty (ViewTypeDef _ s as t)           = "vtypedef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t
     pretty (TypeDef _ s as t ms)            = "typedef" <+> text s <> prettySortArgs as <+> "=" <+> pretty t <> maybeT ms
     pretty (AbsProp _ n as)                 = "absprop" <+> text n <+> prettyArgs as
-    pretty (Assume n NoA e)                 = "assume" </> pretty n <+> "=" </> pretty e
-    pretty (Assume n as e)                  = "assume" </> pretty n <> prettyArgs as <+> "=" </> pretty e
+    pretty (Assume n as e)                  = "assume" </> pretty n <> prettySortArgs as <+> "=" </> pretty e
     pretty (SymIntr _ ns)                   = "symintr" <+> hsep (fmap pretty ns)
     pretty (Stacst _ n t Nothing)           = "stacst" </> pretty n <+> ":" </> pretty t
     pretty (Stacst _ n t (Just e))          = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -45,6 +45,7 @@
     , Fixity (..)
     , StackFunction (..)
     , Sort (..)
+    , SortF (..)
     , SortArg (..)
     , SortArgs
     , DataSortLeaf (..)
@@ -132,7 +133,7 @@
                    | AndD (Declaration a) (Declaration a)
                    | Local a (ATS a) (ATS a)
                    | AbsProp a String [Arg a]
-                   | Assume (Name a) [Arg a] (Type a)
+                   | Assume (Name a) (SortArgs a) (Type a)
                    | TKind a (Name a) String
                    | SymIntr a [Name a]
                    | Stacst a (Name a) (Type a) (Maybe (Expression a))
@@ -204,6 +205,7 @@
              | AtPattern a (Pattern a)
              | UniversalPattern a String [Universal a] (Pattern a)
              | ExistentialPattern (Existential a) (Pattern a)
+             | As a (Pattern a) (Pattern a)
              deriving (Show, Eq, Generic, NFData)
 
 data Paired a b = Both a b
@@ -229,6 +231,7 @@
             | VType a Addendum -- ^ @viewtype@ or @vtype@
             | View a Addendum -- ^ @view@
             | TupleSort a (Sort a) (Sort a)
+            | ArrowSort a (Sort a) (Sort a)
             deriving (Show, Eq, Generic, NFData)
 
 -- FIXME a type for sorts?
@@ -383,7 +386,7 @@
                           }
                           deriving (Show, Eq, Generic, NFData)
 
-join <$> traverse makeBaseFunctor [''Pattern, ''Expression, ''StaticExpression, ''Type]
+join <$> traverse makeBaseFunctor [''Pattern, ''Expression, ''StaticExpression, ''Type, ''Sort]
 join <$> traverse makeLenses [''Leaf, ''Declaration, ''PreFunction, ''Implementation, ''DataPropLeaf, ''Function, ''Type]
 
 exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t
diff --git a/test/data/concurrency.out b/test/data/concurrency.out
--- a/test/data/concurrency.out
+++ b/test/data/concurrency.out
@@ -40,9 +40,9 @@
 extern
 fun {a:t@ype} queue_free (que : queue(a)) : void
 
-assume queue_vtype(a : vt0p, id : int) = deqarray(a)
-assume ISNIL(id : int, b : bool) = unit_p
-assume ISFULL(id : int, b : bool) = unit_p
+assume queue_vtype(a: vt0p, id: int) = deqarray(a)
+assume ISNIL(id: int, b: bool) = unit_p
+assume ISFULL(id: int, b: bool) = unit_p
 
 absvtype channel_vtype(a: vt@ype+) = ptr
 
@@ -84,7 +84,7 @@
 extern
 fun channel_refcount {a:vt0p} (ch : !channel(a)) : intGt(0)
 
-assume channel_vtype(a : vt0p) = channel_
+assume channel_vtype(a: vt0p) = channel_
 
 implement {a} queue_is_nil (xs) =
   (unit_p() | deqarray_is_nil(xs))