Safe Haskell | None |
---|---|
Language | Haskell2010 |
Types
Description
This is still a work in progress.
No really, what's this type system?
Eventually? I want
- Linear
- call-by-push-value with
- arbitrary rank type and kind polymorphism and
- graded (co)effects.
We can take this one at a time.
Linear
Linear logic, seemingly like everything else in academia, is at once a dense subject of study with profound implications, and also a very simple idea.
As it applies to programming the basic idea is to think of types as defining resources, and the values of those types as matter which can't simply be duplicated or discarded (ignored) at will! The arrogance! So if you bind a value to a name in some scope you must use it exactly once within that scope.
Here is what pure linear file I/O would look like in pseudo-code:
file_handle := open_file ("foo.txt"); (file_handle, line_1) := read_line (file_handle); (file_handle, line_2) := read_line (file_handle); close (file_handle);
Notice that file_handle
must be re-bound after each use, because each binding
must be used exactly once.
There are many systems for relaxing and extending this system to other uses, but
that is the basic premise.
The appeal of linear logic in programming circles, it seems, stemmed from the promise of being able to prevent memory leaks statically at compile-time -- if you can't use a pointer twice without explicitly duplicating it, it's hard to use it a million times on accident in a loop!
On the other hand, not being able to write let square x = x * x
without
resorting to a helper utility is a pretty draconian restriction.
One of psilo's goals is to deliver on the promises of linear logic in an
intuitive way such that linearity aids development.
Call-By-Push-Value
Most languages are "strict", or call-by-value: all procedure arguments must be fully evaluated before they may be passed along. There are usually ways to explicitly circumvent this for when a computation needs to be delayed.
Some, like Haskell, are "lazy", or call-by-name/need: a term passed to a function is not evaluated fully until absolutely necessary.
It's why in Haskell, this interactive session terminates:
> fix f = let x = f x in x > bottom = fix id > 1 + (const 2 bottom) 3
bottom
is not actually evaluated by const
and so the fact that it does not
terminate is no matter.
Psilo is both and neither!
Call-by-push-value subsumes both of these and instead encodes evaluation order in the type system.
A positive type is "data": it is defined by the shape of its values. You could conceivably come up with a way to print it out on paper. It's static, at rest.
A negative type is a "computation": it a process executing, a function during application, dynamic, "in motion."
Crucially, the system provides ways to convert a term between these two polarities: for instance, a function might be "suspended" to be "resumed" later, and the resulting thunk could be passed as an argument. Likewise, a static piece of data may be promoted into a do-nothing function that simply returns that value.
And it so happens it combines well with linearity.
All together, say it with me: Linear Call-By-Push-Value!
It turns out that linear types and CBPV very naturally and elegantly pair with one another: positive terms are precisely those which may be duplicated or ignored without a second-thought; negative terms are those which must be treated linearly.
Example: a function λ x. f x
is negative, while its argument x
is positive
and the function term f
is also negative, as is the entire expression f x
.
Coeffects!
It so-happens that you can regard the linear logic I described above as a specialization of a more general idea called coeffects. I call them coeffects because
- Believe it or not that's the term in the literature, and
- The only other appropriate name I can honestly think of is "context" which is the most overloaded term in programming.
You can think of the linear logic described above as a coeffect where each bound term has a number attached to it defining how many times it may be used in a scope.
A more exotic example might be defining an enum of security roles that attach to every term the moment they are created, and rules for then performing security auditing statically at compile time.
A coeffect system is a set of rules for defining contextual data like that, along with the rules for the compiler to then enforce certain constraints.
Part of my current work is figuring out how this integrates with linear CBPV and thus how it should be represented syntactically.
Arbitrary-rank type and kind polymorphism.
I'm out of time for today!
- kinds: the "types of types". Basic types have kind
*
, and a function from typeA : *
toB : *
is itself a third function type,A -> B : * -> * -> *
. - arbitrary rank types: I can write types like, eg
∀A B. (∀R. (A -> R) -> R) -> B
. Future drafts will spell this out more. - "kind polymorphism?" Yeah what, did you think
*
is the only kind?
That sounds like a tall order.
At the moment, besides the rules for shift
and reset
, this module
competently implements a basic version of System F with let-polymorphism.
Once the delimited control operators are settled, the next step will probably be
adding surface syntax for the type language and implementing arbitrary-rank
polymorphism, because in general my inference algorithm will need to be assisted
just a little by the programmer sometimes with type annotations, and I don't
have a type annotation syntax yet.
After that, finally, I'll likely be ready to tackle (co)effects.
Papers and posts I am cribbing from:
Synopsis
- type TypeVar = Int
- data Type
- type Sigma = Type
- type Rho = Type
- type Tau = Type
- ty_int :: Rho
- ty_float :: Rho
- ty_bool :: Rho
- ty_bottom :: Rho
- ty_fun_sig :: [Type] -> Type -> Type
- data Frame = Frame {}
- frame_empty :: Frame
- frame_extend :: Frame -> (Symbol, Type) -> Frame
- frame_remove :: Frame -> Symbol -> Frame
- frame_extends :: Frame -> [(Symbol, Type)] -> Frame
- frame_lookup :: Symbol -> Frame -> Maybe Type
- frame_merge :: Frame -> Frame -> Frame
- frames_merge :: [Frame] -> Frame
- frame_singleton :: Symbol -> Type -> Frame
- frame_keys :: Frame -> [Symbol]
- frames_fromList :: [(Symbol, Type)] -> Frame
- frames_toList :: Frame -> [(Symbol, Type)]
- type Infer = ReaderT Frame (StateT InferState (Except String))
- data InferState = InferState {}
- default_infer_state :: InferState
- newtype Subst = Subst (Map TypeVar Rho)
- type Constraint = (Type, Type)
- type Unifier = (Subst, [Constraint])
- type Solve a = ExceptT String Identity a
- class Substitutable a where
- substitute :: Subst -> a -> a
- ftv :: a -> Set TypeVar
- run_infer :: Frame -> Infer a -> Either String a
- typecheck :: Frame -> CbpvExp -> Either String Type
- close_over :: Type -> Sigma
- normalize :: Sigma -> Sigma
- in_frame :: (Symbol, Type) -> Infer a -> Infer a
- in_frames :: [(Symbol, Type)] -> Infer a -> Infer a
- lookup_in_frame :: Symbol -> Infer (Rho, [Constraint])
- fresh :: Infer Tau
- instantiate :: Sigma -> Infer Rho
- generalize :: Frame -> Rho -> Sigma
- skolemize :: Sigma -> Infer ([TypeVar], Rho)
- infer :: CbpvExp -> Infer (Rho, [Constraint])
- subst_empty :: Subst
- compose :: Subst -> Subst -> Subst
- run_solve :: [Constraint] -> Either String Subst
- unify_many :: [Type] -> [Type] -> Solve Subst
- unifies :: Type -> Type -> Solve Subst
- solver :: Unifier -> Solve Subst
- bind :: TypeVar -> Type -> Solve Subst
- occurs_check :: Substitutable a => TypeVar -> a -> Bool
- solve_inference :: [Constraint] -> (Subst -> Infer a) -> Infer a
- prim_type :: Symbol -> Maybe Sigma
- data Graph node key = Graph {}
- graph_fromList :: Ord key => [(node, key, [key])] -> Graph node key
- vertex_labels :: Functor f => Graph b t -> f Vertex -> f b
- vertex_label :: Graph b t -> Vertex -> b
- topo :: Graph node key -> [node]
- make_dep_graph :: Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol
(basic) Type language
Instances
Eq Type Source # | |
Ord Type Source # | |
Show Type Source # | |
Substitutable Constraint Source # | |
Defined in Types Methods substitute :: Subst -> Constraint -> Constraint Source # | |
Substitutable Type Source # | |
Typing environment ("frame")
frame_empty :: Frame Source #
frames_merge :: [Frame] -> Frame Source #
frame_keys :: Frame -> [Symbol] Source #
Inference monad
data InferState Source #
Constructors
InferState | |
Constraint solving monad
type Constraint = (Type, Type) Source #
type Unifier = (Subst, [Constraint]) Source #
class Substitutable a where Source #
Instances
Substitutable Constraint Source # | |
Defined in Types Methods substitute :: Subst -> Constraint -> Constraint Source # | |
Substitutable Frame Source # | |
Substitutable Type Source # | |
Substitutable a => Substitutable [a] Source # | |
Inference
close_over :: Type -> Sigma Source #
lookup_in_frame :: Symbol -> Infer (Rho, [Constraint]) Source #
skolemize :: Sigma -> Infer ([TypeVar], Rho) Source #
Deep skolemization. Returns the skolem variables and the skolemized ρ-type.
infer :: CbpvExp -> Infer (Rho, [Constraint]) Source #
Type inference rules for CbpvExp
ressions.
All functions have at least one (terminal) argument of type ⊥.
Constraint solver
subst_empty :: Subst Source #
Compose substitutions
Run the constraint solver
Unification solver
occurs_check :: Substitutable a => TypeVar -> a -> Bool Source #
solve_inference :: [Constraint] -> (Subst -> Infer a) -> Infer a Source #
Graph implementation
graph_fromList :: Ord key => [(node, key, [key])] -> Graph node key Source #
vertex_label :: Graph b t -> Vertex -> b Source #