Re: [Haskell-cafe] Re: Amazing
Am Sonntag, 15. Februar 2009 23:00 schrieb Peter Verswyvelen:
But if I understand it correctly, dependent types are a bit like that,
values and types can inter-operate somehow?
With dependent types, parameters of types can be values. So you can define a
data type List which is parameterized by the length of the list (and the
element type):
data List :: Nat - * - * where -- The kind of List contains a type.
Nil :: List 0 el
Cons :: el - List len el - List (succ len) el
And you have functions where the result type can depend on the actual
argument:
replicate :: {len :: Nat} - el - List len el
-- We have to name the argument so that we can refer to it.
So the type of replicate 0 'X' will be List 0 Char and the type of
replicate 5 'X' will be List 5 Char.
Dependent typing is very good for things like finding index-out-of-bounds
errors and breach of data structure invariants (e.g., search tree balancing)
at compile time. But you can even encode complete behavioral specifications
into the types. For example, there is the type of all sorting functions.
Properly implemented Quicksort and Mergesort functions would be values of
this type but the reverse function wouldn’t. Personally, I have also thought
a bit about dependently typed FRP where types encode temporal specifications.
Dependent types are really interesting. But note that you can simulate them to
a large degree in Haskell, although especially dependent functions like
replicate above need nasty workarounds. You may want to have a look at
Haskell packages like type-level.
Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Amazing
This must be why there are no good compilers for dependently typed languages. :) On Sun, Feb 15, 2009 at 9:40 PM, Stefan Monnier monn...@iro.umontreal.ca wrote: So IMO static typing is good, but it's only with functional programming that it really shines. You can go one step further: if you start using dependent types, you'll see that it gets yet harder to get your program to type-check, and once it does, you don't even bother to run it since it's so blindingly obvious that it's correct. Stefan ___ 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: Amazing
How practical is this dependent types thing? I hear a lot about this from really clever people who are usually 10 years ahead of their time :) Actually, back in the eighties when I was an assembly language hacker, I didn't want to switch to Pascal or C since I found the types in those languages too weak. C++ changed that with templates, and then I switched (only to find out that no C++ compiler existed that would not crash on my fully templated programs ;-). What I really wanted was a way to program the type checks myself; verify constraints/assertions at compile time, and if the constraint or assertion could not be done at compile time, get a warning or an error (or bottom if the custom type checking program is stuck in an endless loop ;-) Of course back then I was even more naive than I am now, so those things are easier said than done I guess. But if I understand it correctly, dependent types are a bit like that, values and types can inter-operate somehow? On Sun, Feb 15, 2009 at 9:40 PM, Stefan Monnier monn...@iro.umontreal.cawrote: So IMO static typing is good, but it's only with functional programming that it really shines. You can go one step further: if you start using dependent types, you'll see that it gets yet harder to get your program to type-check, and once it does, you don't even bother to run it since it's so blindingly obvious that it's correct. Stefan ___ 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: Amazing
It's true that you can do program the type checker even more if you have dependent types, but first you should look into what you can do in Haskell. You can do a lot with type classes. -- Lennart 2009/2/15 Peter Verswyvelen bugf...@gmail.com: How practical is this dependent types thing? I hear a lot about this from really clever people who are usually 10 years ahead of their time :) Actually, back in the eighties when I was an assembly language hacker, I didn't want to switch to Pascal or C since I found the types in those languages too weak. C++ changed that with templates, and then I switched (only to find out that no C++ compiler existed that would not crash on my fully templated programs ;-). What I really wanted was a way to program the type checks myself; verify constraints/assertions at compile time, and if the constraint or assertion could not be done at compile time, get a warning or an error (or bottom if the custom type checking program is stuck in an endless loop ;-) Of course back then I was even more naive than I am now, so those things are easier said than done I guess. But if I understand it correctly, dependent types are a bit like that, values and types can inter-operate somehow? On Sun, Feb 15, 2009 at 9:40 PM, Stefan Monnier monn...@iro.umontreal.ca wrote: So IMO static typing is good, but it's only with functional programming that it really shines. You can go one step further: if you start using dependent types, you'll see that it gets yet harder to get your program to type-check, and once it does, you don't even bother to run it since it's so blindingly obvious that it's correct. Stefan ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
