Type Notation

Haskell’s data/newtype/type syntax great compared to most languages, but can get annoyingly verbose when you want to work with incrementally build types, burying your date under extraneous newtype and data wrappers.

Among the annoying points are

  • Inability to use partially applied type synonyms
  • Lack of anonymous data declarations
  • inability to use “exists. x” directly, instead requiring “forall. x” on a data declaration
  • Either, Left, Right are annoyingly long to write, and the type is not infix like (,) is.

This encourages library designers to “bake in” their types, defining them as one flat datatype, instead of building it incrementally so different components can be swapped out. So we’ll use a convenient shorthand for working with type definitions, and forgo some type wrapping/unwrapping in function definitions when the types are clear. (always giving the legitimate haskell definition at the end.)

data 0 (the empty type)
type 1 = ()
(->) has lowest precedence
a + b === Either a b
L === Left
R === Right
a * b === (a,b)
infixl 6 +
infixl 7 *
λx. e === anonymous version of "type AnonymousType x = e"
μf. e === Fix e, without having to worry about the f index being in the last position. where:
data Fix f = Fix {unFix :: f (Fix f)}
∀x. e === "forall x. e"
∃x. e === "data AnonymousType = forall x. e", without the constructors
∂e/∂x === the the type of e with an x punched out. (lookup data type derivatives)
e/~ === the type e quotiented by the relation ~. In some cases, there is a reduced haskell type (ex. Bool/(True == False) === ()), but in most cases it can only be represented as the type e with "instance Eq e where (==) = (~)", and we require that pattern matching not break the equality abstraction.

*More will be added as necessary*


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s