Re: Stronger static types, was Re: [Haskell-cafe] Re: Versioning
On Dec 21, 2006, at 5:03 PM, Jacques Carette wrote: ... What must be remembered is that full dependent types are NOT needed to get a lot of the benefits of dependent-like types. This is what some of Oleg's type gymnastics shows (and others too). My interest right now lies in figuring out exactly how much can be done statically. For example, if one had decent naturals at the type level (ie naturals encoded not-in-unary) with efficient arithmetic AND a few standard decision procedures (for linear equalities and inequalities say), then most of the things that people currently claim need dependent types are either decidable or have very strong heuristics that work [1]. My understanding is that BlueSpec did roughly this. As we're discovering in Fortress, type-level naturals are a big help; faking it really is horrible, as unary representations are unusable for real work and digital representations require a ton of stunts to get the constraints to solve in every direction (and they're still ugly). I for one would welcome a simple extension of Haskell with type-level nats (the implementor gets to decide if they're a new kind, or can interact with * somehow). -Jan-Willem Maessen [PS: hadn't seen the LNCS reference before, thanks to Jacques for sending that along.] smime.p7s Description: S/MIME cryptographic signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Stronger static types, was Re: [Haskell-cafe] Re: Versioning
Yes, Bluespec has efficient type level naturals. But it only has arithmetic and some trivial decision procedures. The slogan is the type checker knows arithmetic, not algebra. It worked pretty well. But you soon get into situations where you need polymorphic recursion of functions with type level naturals. It needs careful consideration (I never implemented that for Bluespec). -- Lennart On Dec 22, 2006, at 14:28 , Jan-Willem Maessen wrote: On Dec 21, 2006, at 5:03 PM, Jacques Carette wrote: ... What must be remembered is that full dependent types are NOT needed to get a lot of the benefits of dependent-like types. This is what some of Oleg's type gymnastics shows (and others too). My interest right now lies in figuring out exactly how much can be done statically. For example, if one had decent naturals at the type level (ie naturals encoded not-in-unary) with efficient arithmetic AND a few standard decision procedures (for linear equalities and inequalities say), then most of the things that people currently claim need dependent types are either decidable or have very strong heuristics that work [1]. My understanding is that BlueSpec did roughly this. As we're discovering in Fortress, type-level naturals are a big help; faking it really is horrible, as unary representations are unusable for real work and digital representations require a ton of stunts to get the constraints to solve in every direction (and they're still ugly). I for one would welcome a simple extension of Haskell with type- level nats (the implementor gets to decide if they're a new kind, or can interact with * somehow). -Jan-Willem Maessen [PS: hadn't seen the LNCS reference before, thanks to Jacques for sending that along.] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Stronger static types, was Re: [Haskell-cafe] Re: Versioning
Brian Hulley wrote: Would it be possible to augment Haskell's type system so that it was the same as that used in Epigram? No, no! Epigram is a wonderfully pure research experiment in one corner of the design space. The corner it is exploring is not particularly Haskell like, though the results of the exploration should bear fruit for Haskell now and then [and it already has]. While I am quite sure Haskell could do with more information in its types, proof requirements cannot be anywhere close to what it is in Epigram. I am convinced there is a Haskell compatible middle road. Also, typing is not the only issue for compile time guarantees. Consider: [Example of coding enumeration as pattern-match vs guards vs ... deleted] This is much more of an engineering issue than a theoretical issue. In some cases (explicit pattern match with no guards), coverage checking is trivial because the language you are dealing with is so simple. In other cases (guards), in general the problem is undecidable, but there are many many particular cases where there are applicable decision procedures. It seems to be a common choice amongst compiler writers to not wade into these waters -- although the people doing static analysis have been swimming there for quite some time. My feeling is that slowly increasing amounts of static analysis will be done by compilers (beyond just types or the current strictness analyses) to include these kinds of total/partial checks on guards, shape analysis, etc. It is already happening, the one question is what will be the speed at which it happens in Haskell. Maybe it is time for ICFP and SAS to be held together. Jacques ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Re: Versioning
| One thing that might become a problem is that the Scrap your | boilerplate approach seems to work only in GHC. I don't think so. Other compilers might not support deriving Data, but you can always write the instance by hand. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Hello Joachim, Wednesday, December 20, 2006, 9:30:02 PM, you wrote: One thing that might become a problem is that the Scrap your boilerplate approach seems to work only in GHC. There's nothing wrong with GHC, but it sounds like I'm committing to a specific compiler right from the start. I'd like to keep the number of choices as high as possible... there are really no choices for real development. many libraries, language extensions and techniques are for ghc only and besides, if the compiler gives me an error message, or the generated code does unexpected things, I'd like to have the possibility to cross-check with a different compiler. you can use Hugs to develop programs - it has much faster compile times, slightly better error messages and good level of language (extensions) compatibility with ghc. parts of programs that are not compatible with Hugs may be conditionally compiled using #ifdef GHC So have other compilers picked up SYB support yet? SYB and Template Haskell are just examples of techniques that make GHC obvious choice. although. SYB may be supported by Hugs too, i'm not sure That said, serialisation is still a hard problem - think long and hard before picking a data format. What would be the problems of choosing the wrong one? With Yhc.Core I used Drift to derve Binary instances, keep a version tag, and if the version tags mismatch refuse to load the data. unless you need specific data format (say for compatibility with existing data sources) you may easily derive Binary instances either with Drift or with TH using libraries i mentioned in previous letter. http://repetae.net/john/computer/haskell/DrIFT/drop/DrIFT-2.1.1.tar.gz http://repetae.net/john/computer/haskell/DrIFT/drift.ps -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Hi there are really no choices for real development. many libraries, language extensions and techniques are for ghc only I develop everything in Hugs, including the Yhc compiler itself. Hugs is great. There are lots of extensions in GHC, but Haskell 98 is a perfectly useable language! So have other compilers picked up SYB support yet? SYB and Template Haskell are just examples of techniques that make GHC obvious choice. although. SYB may be supported by Hugs too, i'm not sure GHC is the only one with inbuilt SYB support. Hugs has deriving Typeable (I think), but not Data. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
On Dec 21, 2006, at 15:53 , Neil Mitchell wrote: Hi there are really no choices for real development. many libraries, language extensions and techniques are for ghc only I develop everything in Hugs, including the Yhc compiler itself. Hugs is great. There are lots of extensions in GHC, but Haskell 98 is a perfectly useable language! I must second this opinion. There's this (false) perception that you need all kinds of extensions to make Haskell usable. It's simply not true. Certain extensions can make your life easier, but that's it. -- Lennart ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Lennart Augustsson wrote: I must second this opinion. There's this (false) perception that you need all kinds of extensions to make Haskell usable. It's simply not true. Certain extensions can make your life easier, but that's it. To write code in Haskell, this is true. However, one of the wonderful things about Haskell is how much the type system helps you. And if you want the type system to help you even more [which, as a programmer having suffered from dynamic typing too long, I really want], those extensions are really needed. In other words, you can program in Haskell just fine without extensions. But if you want that next level in type safety, extensions is where it's at, at least for the kind of code I write. Jacques ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Hi In other words, you can program in Haskell just fine without extensions. But if you want that next level in type safety, extensions is where it's at, at least for the kind of code I write. What level of safety do these type extensions give you? The biggest runtime crasher is probably pattern match failings, something that most of these type extensions don't catch at all! They do give you some safety, but not a massive amount, and not in the places where it would be truely useful. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Lennart Augustsson wrote: On Dec 21, 2006, at 15:53 , Neil Mitchell wrote: Hi there are really no choices for real development. many libraries, language extensions and techniques are for ghc only I develop everything in Hugs, including the Yhc compiler itself. Hugs is great. There are lots of extensions in GHC, but Haskell 98 is a perfectly useable language! I must second this opinion. There's this (false) perception that you need all kinds of extensions to make Haskell usable. It's simply not true. Certain extensions can make your life easier, but that's it. Well, FingerTrees for example, require MPTCs as in pushL :: Measured v a = a - FingerTree v a - FingerTree v a For any kind of object oriented programming you need existentials to separate the interface from the different concrete objects. Also in the code I've written I've often needed higher rank polymorphism and scoped type variables. Sure it's possible to use all kinds of horrific hacks to try and avoid the need for scoped type variables etc but why would anyone waste their time writing difficult obfuscated code when GHC has the perfect solution all ready to use. In other words, what on earth is good about gluing oneself to Haskell98? Life's moved on... Best regards, Brian. -- http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Hi In other words, what on earth is good about gluing oneself to Haskell98? Life's moved on... If you stick to Haskell 98 you can: * Convert your code to Clean (Hacle) * Debug it (Hat) * Run it in your browser (ycr2js) * Document it (Haddock) * Make a cross platform binary (yhc) * Get automatic suggestions (Dr Haskell) ... Sometimes you need a type extension, but if you don't, you do get benefits. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Neil Mitchell wrote: In other words, you can program in Haskell just fine without extensions. But if you want that next level in type safety, extensions is where it's at, at least for the kind of code I write. What level of safety do these type extensions give you? Check out many, many, many of Oleg's postings to the Haskell list. His code expresses this much better than my words can. The biggest runtime crasher is probably pattern match failings, something that most of these type extensions don't catch at all! Array out-of-bounds, fromJust, head on an empty list, and pattern-match failures are in my list of things I wish the type system could help me with. And sometimes it can [again, see Oleg's posts]. But is definitely where I am *eager* to see developments. They do give you some safety, but not a massive amount, and not in the places where it would be truely useful. Unfortunately, I agree. But I'll still take what I can get! Jacques ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Neil Mitchell wrote: Hi In other words, what on earth is good about gluing oneself to Haskell98? Life's moved on... If you stick to Haskell 98 you can: * Convert your code to Clean (Hacle) * Debug it (Hat) * Run it in your browser (ycr2js) * Document it (Haddock) * Make a cross platform binary (yhc) * Get automatic suggestions (Dr Haskell) ... Sometimes you need a type extension, but if you don't, you do get benefits. True, though it would be even better if the usual extensions were more widely supported, though I suppose identifying what's useful and therefore worth supporting is the point of the Haskell Prime process. As an aside I've often thought it would be better if the various components of Haskell compilers/tools would be separated out so that people could effectively build their own compiler tailored more specifically for their needs. Ie lots of smaller projects each dealing with a particular phase of Haskell processing which would be joined together by standard APIs, so that someone could use the latest type system extensions with whole program optimization while someone else could use those same type extensions with a back end designed for graphical debugging etc, and also so that people just interested in developing whole program optimization (for example) wouldn't have to reinvent the ever-more-difficult wheel of lexing/parsing/typechecking/targeting multiple platforms... Best regards, Brian. -- http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Hi True, though it would be even better if the usual extensions were more widely supported, though I suppose identifying what's useful and therefore worth supporting is the point of the Haskell Prime process. Exactly the reason for Haskell Prime. As an aside I've often thought it would be better if the various components of Haskell compilers/tools would be separated out so that people could effectively build their own compiler tailored more specifically for their needs. http://neilmitchell.blogspot.com/2006/12/bhc-basic-haskell-compiler.html I thought the same thing. Note that Yhc already has a lightweight API for manipulating Yhc.Core files and one for Yhc.Bytecode files. Things are moving in that direction slowly. There is also the GHC API approach. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Jacques Carette wrote: Neil Mitchell wrote: The biggest runtime crasher is probably pattern match failings, something that most of these type extensions don't catch at all! Array out-of-bounds, fromJust, head on an empty list, and pattern-match failures are in my list of things I wish the type system could help me with. And sometimes it can [again, see Oleg's posts]. But is definitely where I am *eager* to see developments. If I understand things correctly (admittedly, a big if ;) ) this is kind of the point of dependent types. A type is a set - when you put a type on an expression, you're asserting that the expression evaluates to a member of that set. So, foo :: Integer - Rational, among other things, asserts that the result of foo x (given that x is a member of the set of Integers) is a member of the set of Rationals. But why stop there? Why not be able to say that foo x is a /positive/ rational, or a non-negative rational between 0 and 1? Or, since we're just describing sets, why not explictly allow the set to depend on x? Why not let the result type be the set of rationals r such that 1/r == x? The Curry-Howard isomorphism leads to all of that. A program that outputs some value x is (isomorphic to) a proof that x is a member of some type. We just generally lack a sufficiently powerful type grammar to express that directly in the program. Dependent types let you make the types of output /depend/ on the actual values of the input. Check out Conor McBride and James McKinna's paper The View From the Left, and their work on the Epigram language to see where they've taken this... http://www.dcs.st-andrews.ac.uk/~james/ - fascinating stuff. I agree with you, though - I'm very eager to see further developments along these lines. It's the main reason I started learning Haskell, and I'm absolutely convinced that functional programming and this kind of increasingly strong typing are the way of the future for programming. -- - What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you understand? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Jacques Carette wrote: Lennart Augustsson wrote: I must second this opinion. There's this (false) perception that you need all kinds of extensions to make Haskell usable. It's simply not true. Certain extensions can make your life easier, but that's it. To write code in Haskell, this is true. However, one of the wonderful things about Haskell is how much the type system helps you. And if you want the type system to help you even more [which, as a programmer having suffered from dynamic typing too long, I really want], those extensions are really needed. In other words, you can program in Haskell just fine without extensions. But if you want that next level in type safety, extensions is where it's at, at least for the kind of code I write. Or, to go the other way, if you don't care about type safety, you might as well program in Javascript. -- - What part of ph'nglui bglw'nafh Cthulhu R'lyeh wagn'nagl fhtagn don't you understand? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Stronger static types, was Re: [Haskell-cafe] Re: Versioning
Yes, dependent types have a lot to do with all this. And I am an eager
lurker of all this Epigram.
Scott Brickner wrote:
Jacques Carette wrote:
Array out-of-bounds, fromJust, head on an empty list, and
pattern-match failures are in my list of things I wish the type
system could help me with. And sometimes it can [again, see Oleg's
posts]. But is definitely where I am *eager* to see developments.
I agree with you, though - I'm very eager to see further developments
along these lines. It's the main reason I started learning Haskell,
and I'm absolutely convinced that functional programming and this kind
of increasingly strong typing are the way of the future for programming.
What must be remembered is that full dependent types are NOT needed to
get a lot of the benefits of dependent-like types. This is what some of
Oleg's type gymnastics shows (and others too). My interest right now
lies in figuring out exactly how much can be done statically.
For example, if one had decent naturals at the type level (ie naturals
encoded not-in-unary) with efficient arithmetic AND a few standard
decision procedures (for linear equalities and inequalities say), then
most of the things that people currently claim need dependent types are
either decidable or have very strong heuristics that work [1].
Jacques
[1]
@book{SymbolicAnalysis,
author= {Thomas Fahringer and
Bernhard Scholz},
title = {Advanced Symbolic Analysis for Compilers: New Techniques
and Algorithms for Symbolic Program Analysis and
Optimization},
publisher = pub-SV,
series= {Lecture Notes in Computer Science},
volume= {2628},
year = {2003},
isbn = {3-540-01185-4}
}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Stronger static types, was Re: [Haskell-cafe] Re: Versioning
Jacques Carette wrote: Yes, dependent types have a lot to do with all this. And I am an eager lurker of all this Epigram. Would it be possible to augment Haskell's type system so that it was the same as that used in Epigram? Epigram itself uses a novel 2d layout and a novel way of writing programs (by creating a proof interactively) but these seem orthogonal to the actual type system itself. Also, typing is not the only issue for compile time guarantees. Consider: data Dir = Left | Right | Up | Down deriving Eq -- Compiler can check the function is total foo :: Dir - String foo Left = Horizontal foo Right = Horizontal foo Up = Vertical foo Down = Vertical versus -- Less verbose but compiler can't look inside guards foo x | x == Left || x == Right = Horizontal foo x | x == Up || x == Down = Vertical versus something like: foo (Left || Right) = ... foo (Up || Down) = ... Brian. -- http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Stronger static types, was Re: [Haskell-cafe] Re: Versioning
It's possible to augment Haskell type system to be the one in Epigram. But it would no longer be Haskell. :) And to meet the goals of Epigram you'd also have to remove (unrestricted) recursion from Haskell. -- Lennart On Dec 21, 2006, at 23:46 , Brian Hulley wrote: Jacques Carette wrote: Yes, dependent types have a lot to do with all this. And I am an eager lurker of all this Epigram. Would it be possible to augment Haskell's type system so that it was the same as that used in Epigram? Epigram itself uses a novel 2d layout and a novel way of writing programs (by creating a proof interactively) but these seem orthogonal to the actual type system itself. Also, typing is not the only issue for compile time guarantees. Consider: data Dir = Left | Right | Up | Down deriving Eq -- Compiler can check the function is total foo :: Dir - String foo Left = Horizontal foo Right = Horizontal foo Up = Vertical foo Down = Vertical versus -- Less verbose but compiler can't look inside guards foo x | x == Left || x == Right = Horizontal foo x | x == Up || x == Down = Vertical versus something like: foo (Left || Right) = ... foo (Up || Down) = ... Brian. -- http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
On Wed, Dec 20, 2006 at 07:30:02PM +0100, Joachim Durchholz wrote: Neil Mitchell schrieb: You seem to be describing SYB and not knowing it: http://homepages.cwi.nl/~ralf/syb1/ That basically does exactly what you've requested, in terms of traversing all items when only one matters. Yup, that's exactly what I was looking for. Actually I had seen it a while ago, but didn't remember it now. Thanks. You spoke of changing each element to something of a different type. I don't think SYB can do that. A solution (and a portable one too) might be to parameterize all these types, and make them instances of Functor, Foldable and Traversable (see Data.Foldable and Data.Traversable in the GHC 6.6 documentation). You'd have the labour or writing all those instances (though the trivial instances of Functor and Foldable would suffice). But once you've done that, a range of different traversals would be available. It might be not feasible though. The papers mention that you can't serialize (well, actually unserialize) function values with it. For the envisioned update-through-marshalling process, this would prevent me from ever using function values in data that needs to be persistent, and that's quite a harsh restriction. That's hard to avoid, unless you have a data representation of the functions you're interested in. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
On Dec 20, 2006, at 2:37 PM, Joachim Durchholz wrote: Ross Paterson schrieb: It might be not feasible though. The papers mention that you can't serialize (well, actually unserialize) function values with it. For the envisioned update-through-marshalling process, this would prevent me from ever using function values in data that needs to be persistent, and that's quite a harsh restriction. That's hard to avoid, unless you have a data representation of the functions you're interested in. I could encode functions by their name. I don't think that would scale to a large application with multiple developers, but it's not this kind of project anyway. I'd be reluctant to accept that way if it means adding boilerplate code for every function that might ever be serialized. Since I'm planning to serialize an entire application, I fear that I'd need that boilerplate code for 90% of all functions, so even a single line of boilerplate might be too much. Let me just say here that what you are attempting to do sounds very difficult. As I understand, you want to be able to serialize an entire application at some (predetermined / arbitrary?) point, change some of its code and/or data structures, de-serialize and run the thing afterwards. Doing something like this without explicit language support is going to be hard, especially in a fairly static language like Haskell. I would think Smalltalk, Erlang, or something from the Lisp/Scheme family would be more suitable for this sort of work (caveat, I have little experience with any of these languages). Also, take a look here (http://lambda-the-ultimate.org/node/526) for some related discussion. Regards, Jo Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Versioning
Hi With Yhc.Core I used Drift to derve Binary instances, keep a version tag, and if the version tags mismatch refuse to load the data. Links? http://repetae.net/~john/computer/haskell/DrIFT/ http://darcs.haskell.org/yhc/src/libraries/general/Yhc/General/Binary.hs Thats Drift which can derive binary instances (pick GhcBinary), and then a module which can work with the derived classes. Warning, mild hacking was required to get it going on Windows. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
