[Haskell] PhD position in Communicating Transactions at Trinity College Dublin
Language Support for Communicating Transactions A three year PhD position, to start in September 2011, is now available at Trinity College Dublin, Ireland, associated with the project "Language Support for Communicating Transactions" funded by the Microsoft Research PhD Scholarship scheme. Three years fees will be paid at the EU rate and there will be a stipend at the standard HEA rate. The position is based in the Department of Computer Science at Trinity College, co-supervised by Matthew Hennessy at Trinity and Andrew Gordon and Nick Benton at Microsoft Research, Cambridge England. The goal of the project is to develop abstract models and programming support for "communicating transactions" a novel language construct obtained by dropping the standard isolation requirement from traditional transactions. As a result independent transactions can interfere, or communicate, with each other, which leads to complex interdependences in the event of failure. The goal of the project is to construct abstract models for their behaviour and to develop efficient programming language support for these models. Specifically the project will extend concurrent Haskell with a construct for communicating transactions, study the formal semantics of the extended language, investigate efficient implementation strategies, and develop useful programming idioms and verification techniques. Candidates are expected to have a first-class degree in Computer Science. The project will involve language implementation, the elaboration of formal semantics, and the development of verification techniques. Consequently the successful candidate will have a broad range of skills. These should include language implementation skills, a good knowledge of formal techniques for the specification of language semantics; experience with logic based verification techniques is also desirable. Informal preliminary enquiries may be made to Matthew Hennessy at Trinity College. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Fixpoint combinator without recursion
On Wed, Apr 04, 2007 at 02:57:06PM -0700, Dan Weston wrote: > What is it called if it's both? Is this even legal in Haskell? It seems > as though this would not be a grounded type, going on forever in both > directions. I guess "negative datatype" is being a bit loose with terminology; the function constructor (->) has a negative (also called contravariant) and a positive (covariant) argument; I used "negative datatype" to mean a datatype that has a negative occurence of the data type being defined. It is perfectly valid Haskell and can be quite useful, for instance to define streams, or higher order abstract syntax (HOAS) - but it does have some strange properties, not the least of which is that it gives you recursion :) For that reason, Coq for example forbids negative occurences (because all functions must terminate); this is known as the positivity condition. I don't know which terminology (positive/negative, contravariant/covariant) is more common; I guess it depends on the community. Note that even in a definition where the type being defined is used in both the negative and the positive location, there are perfectly valid and terminating terms of that type: data Foo = Foo (Foo -> Foo ) Here is an instance of Foo: Foo id Edsko ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Fixpoint combinator without recursion
Hey,
It is well-known that negative datatypes can be used to encode
recursion, without actually explicitly using recursion. As a little
exercise, I set out to define the fixpoint combinator using negative
datatypes. I think the result is kinda cool :) Comments are welcome :)
Edsko
{-
Definition of the fixpoint combinator without using recursion
Thanks to Dimitri Vytiniotis for an explanation of the basic principle.
-}
module Y where
{-# NOINLINE app #-}
data Fn a = Fn (Fn a -> Fn a) | Value a
-- Application
app :: Fn a -> Fn a -> Fn a
app (Fn f) x = f x
-- \x -> f (x x)
delta :: Fn a -> Fn a
delta f = Fn (\x -> f `app` (x `app` x))
-- Y combinator: \f -> (\x -> f (x x)) (\x -> f (x x))
y :: Fn a -> Fn a
y f = delta f `app` delta f
-- Lifting a function to Fn
lift :: (a -> a) -> Fn a
lift f = Fn (\(Value x) -> Value (f x))
-- Inverse of lift
unlift :: Fn a -> (a -> a)
unlift f = \x -> case f `app` Value x of Value y -> y
-- Fixpoint combinator
fix :: ((a -> a) -> (a -> a)) -> (a -> a)
fix f = unlift (y (Fn (\rec -> lift (f (unlift rec)
-- Example: factorial
facR f n = if n == 1 then 1 else n * f (n - 1)
fac = fix facR
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Higher kind type inference paper
Hi, Are there any papers that describe how higher kind type inference (and I really mean higher kind, not higher rank) is done? Thanks, Edsko ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Type inference for arbitrary rank types
Hi, I am currently studying the paper "Practical Type Inference for Arbitrary Rank Types" by Simon Peyton Jones and Mark Shields, and I've been wondering about the final version of the typing rules (figure 7, "Bidirectional version of Odersky-Laufer") (although I suppose the question is slightly more general than this figure). In this figure, there are rules for annotated abstractions (AABS1 and AABS2) and annotated terms (ANNOT). What I'm wondering about: are the rules AABS1 and AABS2 really necessary? As in, if you would remove those two rules, does there exist a program that can be typed with the original set of rules than cannot be typed with the set of rules with AABS1/2 removed? It seems to me that any program that can be typed using AABS1/2, can also be typed with ANNOT. More importantly, in the absence of lexically scoped type variables, a type such as forall a. (forall b. (a, b) -> (b, a)) -> [a] -> [a](*) (the example given on page 11, section 4.1 in the paper) cannot even be typed using AABS1/2, but must be typed with ANNOT. Perhaps I am missing something here though, because in Odersky and Laufer's original paper, they do not do "local type inference" (they don't specify a bidirectional version), which would make type (*) impossible to specify in their original system? Thanks, Edsko ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
