Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
On Sat, Mar 14, 2009 at 2:36 AM, Henning Thielemann lemm...@henning-thielemann.de wrote: a lot. However, isn't this halfheartedly since we all wait for full dependent types? :-) Well, in C++ one can already use the numerical values with templates for achieving a lot of compile time computations. So I would be very happy to have this feature in Haskell. It might also be good research towards full dependent types no? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Henning
On 14 Mar 2009, at 01:36, Henning Thielemann wrote:
On Tue, 10 Mar 2009, Conor McBride wrote:
Apologies for crossposting. Please forward this message
to individuals or lists who may be interested. In addition
to the recently advertised PhD position at Strathclyde on
Reusability and Dependent Types, I am delighted to
advertise the following PhD opportunity.
{-
-- Haskell Types with Numeric Constraints
-}
Sounds like it could simplify
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/
dimensional/
Hope so.
a lot. However, isn't this halfheartedly since we all wait for full
dependent types? :-)
Rome wasn't burnt in a day.
Of course I want more than just numerical indexing (and I even
have a plan) but numeric constraints are so useful and have
so much of their own peculiar structure that they're worth
studying in their own right, even for languages which do have
full dependent types, let alone Haskell. We'll carry out this
project with an eye to the future, to make sure it's compatible
with full dependent types.
Be assured (excited, nervous, etc...) that this is not
halfhearted: it's a wholehearted start.
All the best
Conor
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Am Samstag, 14. März 2009 08:19 schrieb Peter Verswyvelen: Well, in C++ one can already use the numerical values with templates for achieving a lot of compile time computations. So I would be very happy to have this feature in Haskell. It might also be good research towards full dependent types no? I doubt that it will be a good thing to include full dependent types into a language with partial functions like Haskell. Conor, is Epigram currently under development? Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Wolfgang On 14 Mar 2009, at 12:00, Wolfgang Jeltsch wrote: Am Samstag, 14. März 2009 08:19 schrieb Peter Verswyvelen: Well, in C++ one can already use the numerical values with templates for achieving a lot of compile time computations. So I would be very happy to have this feature in Haskell. It might also be good research towards full dependent types no? I doubt that it will be a good thing to include full dependent types into a language with partial functions like Haskell. I think we could manage quite a bit, though. It seems reasonable to allow types to contain expressions drawn from a total fragment of the value language. Even a tiny fragment (such the expressions built only from fully applied constructors and variables) would be a useful start (vector head, tail, zip, but not vector append). The present capacity for open type functions suggests that it shouldn't be too violent to add some total value-functions (probably with a flag allowing self-certification of totality). We should also ask what the problem is with partiality? I'd far rather have a simplistic Set-based intuition about what values in types might mean, rather than worrying about vectors of length bottom. The other side of that coin is that it makes perfect sense to have partial *computations* in types as long as they're somehow distinguished from total values, and as long as the system remembers not to *run* them until run-time. My point: it isn't all or nothing -- there's a slider here, and we can shift it a bit at a time. Conor, is Epigram currently under development? We've even stopped working on the engine and started working on the chassis. I'm in an intensive teaching block until the end of April, but from May it becomes Priority. The Reusability and Dependent Types project studentship will hopefully bring an extra pair of hands, come October. Epigram exists to be stolen from, so I'll be trying to encourage a literate programming style and plenty of blogging. We've spent a lot of time figuring out how to make the system much more open and modular, so it will hopefully prove easier for people to contribute to as well as to burgle. The worst thing about Epigram 1 was just how monolithic and impenetrable the code base became. It was a valuable learning experience but no basis for further progress. This time, we optimize for clarity. I don't see any conflict -- indeed I see considerable synergy -- in working simultaneously on the experimental frontier of dependent type systems and on the pragmatic delivery of their basic benefits via a much more established language like Haskell. Indeed, I think we'll learn more readily about the engineering realities of developing applications with dependent types by doing plenty of the latter. I don't think functional programmers should wait for the next generation of languages to mature before picking up this particular habit... All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
On Saturday 14 March 2009 8:12:09 am Conor McBride wrote: Rome wasn't burnt in a day. Of course I want more than just numerical indexing (and I even have a plan) but numeric constraints are so useful and have so much of their own peculiar structure that they're worth studying in their own right, even for languages which do have full dependent types, let alone Haskell. We'll carry out this project with an eye to the future, to make sure it's compatible with full dependent types. One should note that ATS, which has recently been generating some excitement, doesn't have full dependent types, depending on what exactly you mean by that. For instance, it's dependent typing for integers consist of: 1) A simply typed static/type-level integer type 2) A family of singleton types int(n) parameterized by the static type. For instance, int(5) is the type that contains only the run-time value 5. 3) An existential around the above family for representing arbitrary integers. where, presumably, inspecting a value of the singleton family informs the type system in some way. But, we can already do this in GHC (I'll do naturals): -- datakind nat = Z | S nat data Z data S n -- family linking static and dynamic data NatFam :: * - * where Z :: NatFam Z S :: NatFam n - NatFam (S n) -- existential wrapper data Nat where N :: forall n. NatFam n - Nat Of course, ATS' are built-in, and faster, and the type-level programming is probably easier, but as far as dependent typing goes, GHC is already close (I don't think you'd ever see the above scheme in something like Agda or Coq with 'real' dependent types). And this isn't just limited to integers. If you go look at the quicksort example, you'll see something that when translated to GHC looks like: -- datakind natlist = nil | cons nat natlist data Nil data n ::: l data ListFam :: * - * where Nil :: ListFam Nil (:::) :: forall n l. NatFam n - ListFam l - ListFam (n ::: l) data List where L :: forall l. ListFam l - List So this sort of type-level vs. value-level duplication with GADTs tying the two together seems to be what is always done in ATS. This may not be as sexy as taking the plunge all the way into dependent typing ala Agda and Coq, but it might be a practical point in the design space that GHC/Haskell-of-the- future could move toward without too much shaking up. And if ATS is any indication, it allows for very efficient code, to boot. :) Cheers, -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Am Samstag, 14. März 2009 14:51 schrieb Conor McBride: Conor, is Epigram currently under development? We've even stopped working on the engine and started working on the chassis. I'm in an intensive teaching block until the end of April, but from May it becomes Priority. The Reusability and Dependent Types project studentship will hopefully bring an extra pair of hands, come October. This sounds good! I don't see any conflict -- indeed I see considerable synergy -- in working simultaneously on the experimental frontier of dependent type systems and on the pragmatic delivery of their basic benefits via a much more established language like Haskell. Indeed, I think we'll learn more readily about the engineering realities of developing applications with dependent types by doing plenty of the latter. This makes sense indeed. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Dan On 14 Mar 2009, at 14:26, Dan Doel wrote: On Saturday 14 March 2009 8:12:09 am Conor McBride wrote: Rome wasn't burnt in a day. Of course I want more than just numerical indexing (and I even have a plan) but numeric constraints are so useful and have so much of their own peculiar structure that they're worth studying in their own right, even for languages which do have full dependent types, let alone Haskell. We'll carry out this project with an eye to the future, to make sure it's compatible with full dependent types. One should note that ATS, which has recently been generating some excitement, doesn't have full dependent types, depending on what exactly you mean by that. I'm really impressed by the results ATS is getting, and by DML before it. I think these systems do a great job of showing what can be gained in performance by improving precision. For instance, it's dependent typing for integers consist of: I certainly want 1) A simply typed static/type-level integer type which looks exactly like the value-level integers and has a helpful but not exhaustive selection of the same operations. But this... 2) A family of singleton types int(n) parameterized by the static type. For instance, int(5) is the type that contains only the run-time value 5. 3) An existential around the above family for representing arbitrary integers. ...I like less. where, presumably, inspecting a value of the singleton family informs the type system in some way. But, we can already do this in GHC (I'll do naturals): -- datakind nat = Z | S nat data Z data S n -- family linking static and dynamic data NatFam :: * - * where Z :: NatFam Z S :: NatFam n - NatFam (S n) -- existential wrapper data Nat where N :: forall n. NatFam n - Nat Of course, ATS' are built-in, and faster, and the type-level programming is probably easier, but as far as dependent typing goes, GHC is already close (I don't think you'd ever see the above scheme in something like Agda or Coq with 'real' dependent types). Which is why I'd rather not have to do that in Haskell either. It really hurts to go through this rigmarole to make this weird version of Nat. I'd much rather figure out how to re-use the existing datatype Nat. Also, where the GADT coding really doesn't compete with ATS is in dealing with constraints on indices that go beyond unification -- numbers have more structure and deserve special attention. Numerical indexing systems need to carry a big stick for boring algebra if we're to gain the power but keep the weight down. But wherever possible, I'd prefer to avoid doing things an awkward way, just because we don't quite have dependent types. If the above kludge is really necessary, then it should at least be machine- generated behind the scenes from ordinary Nat. I'd much rather be able to lift a type to a kind than have a separate datakind feature. Apart from anything else, when you get around to indexed kinds, what you gonna index /them/ with? Long term, I'd far rather think about how to have some sort of dependent functions and tuples than muddle along with singletons and weak existentials. So this sort of type-level vs. value-level duplication with GADTs tying the two together seems to be what is always done in ATS. This may not be as sexy as taking the plunge all the way into dependent typing ala Agda and Coq, but it might be a practical point in the design space that GHC/Haskell- of-the- future could move toward without too much shaking up. And if ATS is any indication, it allows for very efficient code, to boot. :) I'd certainly agree that ATS demonstrates the benefits of moving in this direction, but I think we can go further than you suggest, avoiding dead ends in the design space, and still without too much shaking up. I don't think the duplicate-or-plunge dilemma you pose exhausts the options. At least, I seem no reason to presume so and I look forward to finding out! To be honest, I think the real challenge is to develop good libraries and methodologies for working with indexed types (and particularly, indexed notions of computation: what's the indexed mtl?). There are lots of promising ideas around, but it's hard to build something that scales whilst the encodings are so clunky. A bit of language design, even just to package existing functionality more cleanly, would really kick the door open. And yes, I am writing a research proposal. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
On Saturday 14 March 2009 1:07:01 pm Conor McBride wrote: But this... 2) A family of singleton types int(n) parameterized by the static type. For instance, int(5) is the type that contains only the run-time value 5. 3) An existential around the above family for representing arbitrary integers. ...I like less. Well, I don't actually like it, either. Finding this out rather disappointed me. I'd certainly agree that ATS demonstrates the benefits of moving in this direction, but I think we can go further than you suggest, avoiding dead ends in the design space, and still without too much shaking up. I don't think the duplicate-or-plunge dilemma you pose exhausts the options. At least, I seem no reason to presume so and I look forward to finding out! I didn't mean to suggest that ATS is the best you can do. Merely that you can still get a lot done without going very far beyond what is technically possible (though not enjoyable) in GHC today (to the point that people will actually categorize your language as dependently typed when it merely has a type language comparable in richness and convenience to the value level, but is still mostly separate). So adding more faux dependent typing (like ATS or Omega) isn't just wasting time when we should be figuring out how to compile Agda efficiently, because simply making type-level programming easy, while maintaining a strict divide between values and types may well be good enough in practice, until the Agdas and Epigrams come into their own. If you can do better than ATS, and have value-level stuff automatically reproduced at the type level and suchlike, so much the better. I fully support that. :) -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
the nearly dependent near future, was Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Dan
On 14 Mar 2009, at 18:48, Dan Doel wrote:
On Saturday 14 March 2009 1:07:01 pm Conor McBride wrote:
I don't think the duplicate-or-plunge dilemma you
pose exhausts the options. At least, I seem no reason to presume
so and I look forward to finding out!
I didn't mean to suggest that ATS is the best you can do. Merely
that you can
still get a lot done without going very far beyond what is technically
possible (though not enjoyable) in GHC today (to the point that
people will
actually categorize your language as dependently typed when it
merely has a
type language comparable in richness and convenience to the value
level, but
is still mostly separate).
I'd certainly agree with that assessment.
[..]
If you can do better than ATS, and have value-level stuff
automatically
reproduced at the type level and suchlike, so much the better. I
fully support
that. :)
Good! 'Cos that's what I'm going for. It certainly won't involve types
depending on arbitrary expressions -- or even on run-time data in the
first instance -- but by taking the approach of lifting what we can
from types to kinds and from values to types, we keep those options
open, as well as hiding the cruft.
Note: subject about to slide into something a tad more technical, but
I gotta tell you this one...
To echo your remarks above, I'm pretty sure one could go quite far even
with something as non-invasive as a GHC preprocessor. My opening gambit
would be to extend the grammar of kinds as follows, with a translation
(#) back to current kinds:
kind ::= * #* = *
| kind - kind #(j - k) = #j - #k
| {type}#{t}= *
| forall x :: kind. kind#(forall x :: j. k) = #k
Note that this forall abstracts type-level stuff in a given kind, not
kinds themselves, so the bound variable can only occur inside the {..}
used to lift types up to kinds. Correspondingly, when we smash the {t}
kinds all to *, we can dump the polymorphism.
Now populate the {t} kinds by lifting expressions to the type level:
these look like {e} where e :: t is built from fully applied
constructors and variables. That's certainly a total fragment!
The preprocessor will need to cook up the usual bunch of gratuitous
type constructors, one for each data constructor used inside {..} in
order to translate expressions to types. It will need to perform
tighter checks on class and data declarations (ideally by constructing
objects one level down which express an equivalent typing problem)
but GHC already has the necessary functionality to check programs.
It might be possible to cut down on the amount of {..} you need to
festoon your code with. On the other hand, it might be good to delimit
changes of level clearly, especially given existing namespace policies.
It's not much but it's a start, it's super-cheap, and it's compatible
with a much more sophisticated future. I program in this language
already, then I comment out the kinds and types I want and insert
their translations by hand. At the moment, I have to write types like
data Case :: ({a} - *) - ({b} - *) - {Either a b} - * where
InL :: f {a} - Case f g {Left a}
InR :: g {b} - Case f g {Right b}
rather than programs like, er... either. But perhaps we could
also figure out how to translate either to a type function.
However, the numeric constraints project will need more than a
preprocessor, because it delivers specific new constraint-solving
functionality during type inference, rather than just the precooking
of first-order value unification problems as first-order type
unification problems. Indeed, with rank-n types, it could be quite
fun.
I'm sure there are devils yet in details, but the prospects for
not-quite-dependent types by re-use rather than hard labour look
quite good, and forwards-compatible with yer actual dependent
functions, etc, further down the line.
We live in interesting times!
All the best
Conor
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
On Tue, 10 Mar 2009, Conor McBride wrote:
Apologies for crossposting. Please forward this message
to individuals or lists who may be interested. In addition
to the recently advertised PhD position at Strathclyde on
Reusability and Dependent Types, I am delighted to
advertise the following PhD opportunity.
{-
-- Haskell Types with Numeric Constraints
-}
Sounds like it could simplify
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/dimensional/
a lot. However, isn't this halfheartedly since we all wait for full
dependent types? :-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hello Conor,
Tuesday, March 10, 2009, 6:59:58 PM, you wrote:
{-
-- Haskell Types with Numeric Constraints
-}
are you have in mind integrating results into production ghc versions?
--
Best regards,
Bulatmailto:bulat.zigans...@gmail.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Bulat, hi all,
On 10 Mar 2009, at 16:06, Bulat Ziganshin wrote:
Hello Conor,
Tuesday, March 10, 2009, 6:59:58 PM, you wrote:
{-
-- Haskell Types with Numeric Constraints
-}
are you have in mind integrating results into production ghc versions?
Subject to rigorous quality control, community approval,
and Official Permission, yes. We'll prototype first, of
course, but the Microsoft sponsorship provides an ideal
opportunity to work with GHC HQ on this. If we do a good
job (so we need a good student) it should become part of
the real deal.
Only this morning, I was lecturing on combinators for
2-dimensional layout and apologizing for the need to
manage the sizes for perfect fitting by smart
constructor abstraction rather than typing. I really
want to rectify that. I can imagine similar
considerations affect hardware design libraries too,
and goodness knows what else. Wire up numerical indexing
to parametrized monads and not only are you cooking with
gas, you might even know how much gas you're cooking with!
So, yes. It's type-level integers that don't suck, and
associated programming techniques, to be delivered via
GHC and associated libraries. This is a real opportunity
to make a difference (and also to stare out the window
and watch the sun setting on central Glasgow, unless it's
raining, which today it isn't).
All the best
Conor
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
