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: 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
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
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: 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
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
