We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:
"The PhD student will join the Programming Logic group and contribute
to its research on dependent type theory and functional programming.
Topics of interest
==
VACANCY : 1x Phd position in dependent types, testing & hardware design
==
The research group of Software Technology is part of the Software
Systems division of in
Am Samstag, 14. Juli 2007 23:04 schrieb Vivian McPhail:
> […]
> They say that haskell programmers are normally averse to dependent types.
So I’m far away from being normal.
> […]
> What are peoples' thoughts on adding dependent types to haskell as a
> non-incremental e
kell programmers are normally
> averse
> to dependent types. Is this true? It seems to me that one of the appeals
> of Haskell is the ability to program in a "prove perfect, write once"
> (elegant) style. Is not dependent typing a good move towards this goal?.
> It addresses
Hello,
As the authors point out [1], coal-face time needs to be expended before
real world adoption of Dependently-Typed functional programming. But let's
get the ball rolling. They say that haskell programmers are normally averse
to dependent types. Is this true? It seems to me that o
An earlier message showed an example of writing code with non-trivial
static guarantees in the present-day Haskell (i.e., Haskell98 + rank-2
types).
http://pobox.com/~oleg/ftp/Haskell/types.html#branding
Although this approach obviously falls short of the genuine dependent
typing, we can
>I think you are confusing Dependent Types with Functional Dependencies.
Actually the two are not that dissimilar... If we allow types to depend
on types (which is what Functional Dependencies allow) IE:
class a b | a -> b
instance Int Float
instance Float In
On Fri, Aug 27, 2004 at 10:26:51AM -0400, Michael Manti wrote:
> I recognize that I'm far out of my depth here--both in Haskell and in
> mathematics--but I'll ask anyway. In what ways are dependent types
> (http://haskell.org/hawiki/FunDeps,
> http://www.cse.ogi.edu/
I recognize that I'm far out of my depth here--both in Haskell and in mathematics--but
I'll ask anyway. In what ways are dependent types (http://haskell.org/hawiki/FunDeps,
http://www.cse.ogi.edu/~mpj/pubs/fundeps.html) insufficient to address these issues?
On Friday, August 27, 2
time.
Matrix length are one of many commonly occuring dependent types in
mathematics. Variable names for polynomials, expansion point and 'scale'
for generalized series expansions, coefficient ring for normalization and
factorization of polynomials, and so on up the food chain. The dependen
Martin Sulzmann stated the goal of the append exercise as follows:
] Each list carries now some information about its length.
] The type annotation states that the sum of the output list
] is the sum of the two input lists.
I'd like to give a Haskell implementation of such an append
function, wh
>This will only work for terminating programs!
Interesting point, but thats because all the operations are at
the type level - therefore if a type is unknown at compile time
we cannot produce a program.
With this type class stuff values can depend on types, but
not the other way around. You can
Hi Martin
Martin Sulzmann wrote:
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
[..]
We'd like to statically guarantee that the sum of the output list
i
The append example is meant to make a general point about
the connection between dependent types and Haskell with
extensions.
I know that the example itself is rather trivial, and
DML/index types, Omega, Haskell+GAD and Chameleon might
seem as too big canons for a rather small target
Actually the data statement wasnt quite right:
data Cons a b = Cons a b
Would work, but now there is nothing keeping each
element in the list as the same type,
I guess we could add a class to constrain to a normal list,,,
class List l x
instance List Nil x
instance List l x => List (Cons x l) x
Just a couple of quick points...
Why store the length along with the list, the length is stored
using type level naturals (Succ | Zero) but these are identical
to the recursion pattern in a List (Cons | Nil) - therefore it
is no less work than having a length function which converts
from one to th
There's a potentially confusing typo.
> append Nil ys = Nil
should be replaced by
append Nil ys = ys
Thanks to Ketil for pointing this out.
Martin
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
-- append.hs
-- append in Haskell
data List a = Nil
| Cons a (List a)
append :: List a ->
etrize the data-structures by their size,
represented as ordinary numbers. Statically expressing the constraints
is easy.
The abstract `brand' is just a type-level proxy for the bounding
interval, and the library of operations provides interval-respecting
operations on indices. This is a very neat so
Hello!
Bjorn Lisper wrote:
> What is the relation to the sized types by Lars Pareto and John Hughes?
It is orthogonal and complementary, as the message in response to
Conor T. McBride indicated.
> What is the relation to classical range analyses for (e.g.) array index
> expressions, which have
Hello!
> What if I don't trust your kernel? The guarantees you require of
> your kernel are not statically checked. What guarantee do I have
> that the propositions which you identify are even the ones which
> are really needed to eliminate bounds checking? How does the
> machine replace ! by uns
In article <[EMAIL PROTECTED]>,
Bjorn Lisper <[EMAIL PROTECTED]> wrote:
>( A really interesting post on static elimination of array bounds checking
>by Oleg...)
>
>Some questions and suggestions:
>
Am I right suspecting, that this method also solves the problem of assuring
the right p in p-modula
search', taken from the famous paper "Eliminating
Array Bound Checking Through Dependent Types" by Hongwei Xi and Frank
Pfenning (PLDI'98). Hongwei Xi's code was written in SML extended
with a restricted form of dependent types. Here is the original code
of the example (t
( A really interesting post on static elimination of array bounds checking
by Oleg...)
Some questions and suggestions:
What is the relation to the sized types by Lars Pareto and John Hughes?
What is the relation to classical range analyses for (e.g.) array index
expressions, which have been know
, quantified type variables, and a compact
general-purpose trusted kernel.
Our example is `bsearch', taken from the famous paper "Eliminating
Array Bound Checking Through Dependent Types" by Hongwei Xi and Frank
Pfenning (PLDI'98). Hongwei Xi's code was written in SML extend
On Wed, Apr 14, 2004 at 06:29:38PM +0200, Tomasz Zielonka wrote:
> >
> > Is it possible to unwrap an existential type in ghci?
>
> For me this seems to be a bug in GHCi.
> I wonder if there a type in Haskell-with-extensions that could be
> assigned to x?
Probably GHCi could do the same as in thi
> > anyway (thus providing the dictionary) there is no point in storing it.
>
> Aren't you talking about a different declaration?
>
> data Show a => Show' a = Show' a
Yes, I am. Oops, sorry.
--KW 8-)
--
Keith Wansbrough <[EMAIL PROTECTED]>
http://www.cl.cam.ac.uk/users/kw217/
University of
On Wed, Apr 14, 2004 at 10:13:51AM -0400, John D. Barnett wrote:
>
> *DepTest> :t Show' True
> Show' True :: Show'
> *DepTest> Show' x <- return $ Show' True
> *DepTest> :t x
> x :: forall a. a
> *DepTest> x
> getTcTyVar a {- tv aXJ -}
> getTcTyVar a {- tv aXJ -}
> getTcTyVar a {- tv aXJ -}
> getT
On Wed, Apr 14, 2004 at 04:58:55PM +0100, Keith Wansbrough wrote:
> > data Show' = forall a . Show a => Show' a
>
> The "forall a. Show a =>" context here has no effect on the
> representation; it merely constrains applications of the data
> constructor Show'. Since you have to say
>
> > print
> data Show' = forall a . Show a => Show' a
The "forall a. Show a =>" context here has no effect on the
representation; it merely constrains applications of the data
constructor Show'. Since you have to say
> print' :: Show' -> IO ()
anyway (thus providing the dictionary) there is no point in
Hello all-
I'm still playing with simulating dependent types using rank-2
polymorphism, and I've run into a small stumbling block on unwrapping
existential datatypes: they can't be let-bound (monomorphic
restriction?), but can be unwrapped in a case or lambda. Actually, I
find
> ...
> This gets at the crux of my questions:
>
> - Why can't the compiler tell that (ListT a, Num b) is enough to figure
> out the additional context it seems to need?
>
Most likely, GHC won't "apply"
> instance (ListT a, Eq b) => Eq (a b)
cause of the overlap.
> - Would it be
Hello-
I'm interested in simulating dependent types in haskell, with the aim of
operating on (as Oleg put it) "stanamically" sized lists: types reflect
size constraints, but ultimately need to be resolved from dynamic input.
I have a good handle on how to do this (read on), but
Robin,
Thanks very much for this. My problem turned out to be tripping over the
monomorphism restriction. When I looked at this it looked like a candidate
for dependent types but as you point out you can solve this just as well in
Haskell 98. You save a set of brackets with my approach
"Dominic Steinitz" <[EMAIL PROTECTED]> wrote:
> I've managed to crack something that always annoyed me when I used to do
> network programming.
[. . .]
>
> Suppose I want to send an ICMP packet. The first byte is the type and the
> second byte is the code. Furthermore, the code depends on the typ
| Here's a bit of background I managed to dig up:
|
http://www.mail-archive.com/haskell@haskell.org/msg05160.html
| It appears that a change to the monomorphism
| restriction to match Hugs's behaviour was considered for
| Haskell 98, but it looks like it never made it into the report
|
> I think you're running into a well-known(*) problem with Hugs's
> implementation of the monomorphism restriction.
>
> (*) actually I thought this was a well-known problem, but it doesn't
> seem to be mentioned in the Hugs documentation as far as I can see.
Here's a bit of background I managed t
> However, if I now comment out the functional dependency
>
> class Encode a b {- | a -> b -} where
>encode :: a -> b
>
> and include the expressions
>
> x = encode TimeExceeded ExcTTL
>
> main = putStrLn x
>
> then Hugs complains
>
> ERROR "codes.hs" (line 37): Unresolved top-level over
I've managed to crack something that always annoyed me when I used to do
network programming. However, Hugs and GHC behave differently. I'd be
interested in views on this approach and also which implementation behaves
correctly.
Suppose I want to send an ICMP packet. The first byte is the type an
At 2001-09-29 17:07, Mike Gunter wrote:
>class Add a b c | a b -> c where add :: a -> b -> c
>instance Add Integer Integer Integer where add = (+)
>pt1 = (3::Integer) `add` (4::Integer) -- Works fine,
>--ft2 = (5::Integer) `add` 6-- Fails
OK, you're running across a fundamental des
> >There does not seem to be a way to do everything I'd like in GHC even
> >in its most permissive mode (I'm using "-fallow-overlapping-instances
> >-fallow-undecidable-instances".) In particular, I'd like to use bare
> >integer literals together with values of the types I define.
>
> Do you ha
At 2001-09-29 09:11, Mike Gunter wrote:
>There does not seem to be a way to do everything I'd like in GHC even
>in its most permissive mode (I'm using "-fallow-overlapping-instances
>-fallow-undecidable-instances".) In particular, I'd like to use bare
>integer literals together with values of th
> You know about fundeps, right? This may help:
>
> class Add a b c | a b -> c where {add :: a -> b -> c;};
Indeed, it's quite hopeless without fundeps. They don't solve with
the ambiguous-literal problem, though.
mike
___
Haskell mail
At 2001-09-29 09:11, Mike Gunter wrote:
> class Add a b c where add :: a -> b -> c
>
>There does not seem to be a way to do everything I'd like in GHC even
>in its most permissive mode (I'm using "-fallow-overlapping-instances
>-fallow-undecidable-instances".) In particular, I'd like to use b
defined elsewhere (which are expecting an
Int/Integer/Double/...)
I think (I have no experience here!) I'd be happiest if GHC
implemented dependent types. That would seem to solve this problem
and others. Even if this broke most Haskell 98 code, I think I'd
turn on the -fdependent-types o
you really need types that
> > > depend on parameters (in particular, integer parameters). This is,
> > > indeed, a problem--currently, you have to do runtime checks.
> > >
> > > Full-fledged dependent types à la Cayenne are undecidable, but there
> > &
Sent: Tuesday, August 15, 2000 2:27 PM
To: [EMAIL PROTECTED]
Cc: [EMAIL PROTECTED]
Subject: basAlgPropos, dependent types
Dear haskellers,
I suggest the two points to your attention.
New basAlgPropos
materials reside in
http://www.botik.ru/pub/local/Mechveliani/basAlgPr
implementation. So, OK, let it exist in an in-complete form.
Attempt with dependent types
This may present an alternative to the sample argument approach used
in basAlgPropos.
I experimented with Cayenne, for several days and remain in a doubt.
I understand few in
There was earlier some discussion on the Basic algebra proposal
(basAlgPropos), in particular, about the Sample argument approach
(SA).
This SA is somehow opposed by the Haskell community.
On the other hand, it may occur that the dependent types, Cayenne
provide some alternative
On 28-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
>
> I downloaded the NU-Prolog manual and skimmed it, but I didn't see the
> features you're describing (probably because I haven't "done" Prolog
> since my learn-5-languages-in-a-quarter class 12 years ago). Could
> you give me a pointer
Fergus Henderson <[EMAIL PROTECTED]> writes:
> > Could you give an example of language syntax that you feel would be
> > better than putting these properties in the type system, while still
> > allowing similar compile-time checking?
>
> I already gave NU-Prolog and Eiffel as examples.
> Those l
Lennart Augustsson <[EMAIL PROTECTED]> writes:
> > (I believe that there are type
> > theories with dependent types, such as the one in Thompson's _Type
> > Theory and Functional Programming_, where each term has at most one
> > type; so it can't just be
> So what does Cayenne do if you don't declare the type for `push'?
> Does it report an error?
The basic principle in Cayenne is that you need type signatures
everywhere. This is sometimes rather verbose and is relaxed
in some cases, but not here. If you omit the type signature
the compiler wi
On 25-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> [someone wrote:]
> > I've lost track of what we're talking about here. In what system can
> > we not hope for principal types?
>
> [...] Cayenne doesn't have that property.
> Again, I think this is a feature, not a bug. I'll incl
On 26-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> > This occurs because in the absense of type declarations,
> > Haskell assumes that any recursion will be monomorphic,
> > which is in general not necessarily the case.
>
> As I'm sure you know, type inference is in general impossi
> (I believe that there are type
> theories with dependent types, such as the one in Thompson's _Type
> Theory and Functional Programming_, where each term has at most one
> type; so it can't just be dependent types that disallow principal
> types.)
The more I thi
The key issue in Lennart's example, I think, is monomorphic recursion.
For the function
f _ =
let y = f 'a'
in undefined
Haskell incorrectly (IMHO) infers the type `f :: Char -> a'
instead of the more general type `f :: b -> a'.
This occurs because in the absens
On 25-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> Fergus Henderson <[EMAIL PROTECTED]> writes:
>
> > Certainly a language with dependent types should define exactly what
> > types the type checker will infer. But when generating code, the
> > comp
> This occurs because in the absense of type declarations,
> Haskell assumes that any recursion will be monomorphic,
> which is in general not necessarily the case.
As I'm sure you know, type inference is in general impossible
for polymorphic recursion, and since Haskell insists on
decidable type
> I've lost track of what we're talking about here. In what system can
> we not hope for principal types? (I believe that there are type
> theories with dependent types, such as the one in Thompson's _Type
> Theory and Functional Programming_, where each term ha
On 25-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> Fergus Henderson <[EMAIL PROTECTED]> writes:
>
> > The basic problem that I have with this is that although dependent types
> > do allow you to specify a lot of things in the type system, I'm not sur
On 25-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
>
> I'm not asking the compiler to deduce anything. I'm talking about run-time
> type matching; this is dynamic types!
Hmm, that seems to be different to what you said last time.
Let me quote:
[Nick Kallen:]
> [Fergus:]
> 2) Yes, I agree that the possibility that user-supplied type
> declarations can change the meaning of the program is a strike against
> the idea.
I don't find that so strange. If there are no principal types
(which we can't hope for), then user added signatures can
have the effect of changing
ume that any language with this feature would have a
> precise specification of type inference sufficient to determine which
> of the two cases was used. Without such a specification, portable
> programming with dependent types is impossible; programs would compile
> under one "smar
Fergus writes:
> I think it's becoming clear by now that the theoretical disadvantages
> of undecidable type checking are often not significant in practice.
> Experience with C++, Gofer, ghc, Mercury, etc. all seems to confirm this.
In this context, people may find the paper _C++ Templates as Pa
ope for), then user added signatures can
> > have the effect of changing the meaning of a program.
>
> I've lost track of what we're talking about here. In what system can
> we not hope for principal types? (I believe that there are type
> theories with dependent ty
e not hope for principal types? (I believe that there are type
theories with dependent types, such as the one in Thompson's _Type
Theory and Functional Programming_, where each term has at most one
type; so it can't just be dependent types that disallow principal
types.)
> BTW, Haskel
"Nick Kallen" <[EMAIL PROTECTED]> writes:
> > Watch out here; there may be a limit to how much run-time type
> > inspection it is reasonable to do in the presence of dependent types.
> > Suppose you're examining a type which happens to be the type of
"Nick Kallen" <[EMAIL PROTECTED]> writes:
> > > > If this is true, then what I'm doing is horrible. But I don't
> > see how this
> > > > leads to nondeterminism or broken referential transparency.
> > min2 returns the
> > > > same value for the same list, but it's simply more efficient
> > if we
Fergus Henderson <[EMAIL PROTECTED]> writes:
> Certainly a language with dependent types should define exactly what
> types the type checker will infer. But when generating code, the
> compiler ought to be able to make use of more accurate type information,
> if it ha
> I don't understand. What behaviour is different here?
>
> Certainly the type is different. But how is the behaviour different?
It behaves differently in that it accepts and returns more/less values. If
this function is part of a program, then the behavior of the program is now
different in th
Lennart Augustsson <[EMAIL PROTECTED]> writes:
> One solution, admittedly somewhat of a hack, is to be able
> to mark one of the components of a record as being the
> essential one. E.g.
> sort :: (l :: [a]) -> sig { *r :: [a]; s :: Sorted l r }
> where the * marks the essential component. Th
formal methods to any extent he desires, with theorem
> > proving being equivalent to the program type checking.
>
> The basic problem that I have with this is that although dependent types
> do allow you to specify a lot of things in the type system, I'm not sure
> that using the t
hat the compiler does.
I'm not asking the compiler to deduce anything. I'm talking about run-time
type matching; this is dynamic types!
> I would assume that any language with this feature would have a
> precise specification of type inference sufficient to determine which
> of
compiler does.
> >
> > I would assume that any language with this feature would have a
> > precise specification of type inference sufficient to determine which
> > of the two cases was used. Without such a specification, portable
> > programming with dependent types is
> Watch out here; there may be a limit to how much run-time type
> inspection it is reasonable to do in the presence of dependent types.
> Suppose you're examining a type which happens to be the type of some
> sorting function:
> (Ord a) => (l :: [a]) -> ((l' :
Lennart Augustsson <[EMAIL PROTECTED]> writes:
> Let me just point out that my main interest in dependent types is
> NOT to do specifications and proofs (like sort above), but to
> make the type system more expressible. This way we can make more
> programs typeable, and also
to Cayenne (theoretically) just by allowing the
^ dynamic?
> run-time type inspection that you intentionally disallowed. In my mind,
> you'd kill two birds with one stone.
Watch out here; there may be a limit to how much run-time type
inspection it is reasonable to do in
depend on the
> amount of inlining etc. that the compiler does.
I would assume that any language with this feature would have a
precise specification of type inference sufficient to determine which
of the two cases was used. Without such a specification, portable
programming with dependent
[EMAIL PROTECTED] writes:
> [EMAIL PROTECTED] writes:
>
> > enabling types to express all properties you want is, IMO, the right way.
>
> Why do I feel that there must be another approach to programming?
>
> How many people do you expect to program in Haskell once you are done adding all
> it
On 22-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> > > min2 :: [a] -> a
> > > min2 ((l:ls) :: [a] <= Sorted) = l
> > > min2 l = min l
> >
> > What's the semantics of that supposed to be?
> > If the list is not known to be definitely sorted,
> > will it check sortedness at runtime?
>
> No.
>
On 22-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> min2 :: [a] -> a
> min2 ((l:ls) :: [a] <= Sorted) = l
> min2 l = min l
What's the semantics of that supposed to be?
If the list is not known to be definitely sorted,
will it check sortedness at runtime?
If not, then the semantics could be
> > min2 :: [a] -> a
> > min2 ((l:ls) :: [a] <= Sorted) = l
> > min2 l = min l
>
> What's the semantics of that supposed to be?
> If the list is not known to be definitely sorted,
> will it check sortedness at runtime?
No.
> If not, then the semantics could be nondeterministic,
> in general, so
On 20-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> [Lennart wrote:]
> > [Nick Kallen wrote:]
> > > To what
> > > extent will a program that type checks completely fail to follow its
> > > specification? Can someone give specific examples?
> >
> > It's trivial to construct examples. Take sor
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> [Fergus wrote:]
> > Well, yes, up to a point, but it may be clearer if the simple
> > regular types part is kept separate from the undecidable part,
> > as was done in NU-Prolog, or as is done in Eiffel.
>
> I'm not necesssarily ad
#x27; :: a -> _) = f
apply' = apply . dynamic
I also think that the notion of dynamic types is quite straightforward
to understand (particularly for programmers with experience in other
languages that support similar constructs, e.g. Java, C++, Eiff
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> > (i.e., you leave out the pivot [x])
> >
> > Obviously the result of sort will no longer be a permutation of its
> > argument. Will this then not type check?
>
> No, the proof (whereever it is) would no longer type check.
As I u
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> > > > F a * = member (map (F a) [0..]) // member [a] a -> Bool
> > > I mave no clue what this means. What is `member'?
> >
> > Member is memq, in, etc. Checks for membership in a list.
> I'm still lost. What is // and how does i
> ...I thought about this pretty hard. Particularly I thought about using
> classes; this was fruitless. So I decided I'd invent a new language feature
> and a nice little syntax to handle it.
>
> Sorted l r = Ordered r /\ Permutation l r
>
> sort :: (l :: [a]) -> (r :: [a]) <= Sorted l r
You'v
[EMAIL PROTECTED] wrote:
> > enabling types to express all properties you want is, IMO, the right way.
>
> Why do I feel that there must be another approach to programming?
>
> How many people do you expect to program in Haskell once you are done adding all
> it takes to "express all imaginable
> I consider even the second one to be mixing the proofs
> with the code, because there's no easy way that I can tell at
> a glance that `sortReallySorts' is a proof rather than a program.
But I consider that a feature and not a bug. :-)
-- Lennart
> > No, the proof (whereever it is) would no longer type check.
>
> As I understand it, this is not necessarily true:
> if the proof contains loops, it might type check,
> even though it is not really a valid proof.
You're right. If the proof is looping it will still
pass as a proof.
-- L
> I believe "//" here is a C++/Java/C9X-style comment.
> Just read it as if "//" were "--". Everything from
> the "//" until the end of line is a comment.
Wow! That's it. Since (//) is an operator on arrays
in Haskell I was trying to make sense out of it, and
failed miserably. :-)
--
thwhile: an official coding style wrt/ dynamics is a good thing, imo.
> I also think that the notion of dynamic types is quite straightforward
> to understand (particularly for programmers with experience in other
> languages that support similar constructs, e.g. Java, C++, Eiffel, etc.)
> wher
> If you return the same proof of correctness that you used
> for the earlier definition of sort, then no it won't type check.
> But if you return a proof defined as e.g.
>
> proof = proof
>
> then if I understand things correctly it will type check.
On that note, since this has been of i
> Well if the ComplicatedTypeToSpecifySorting is correct (I don't know if
> this is possible, but I suspect it isn't) it will of course not type check.
Of course it is possible. The types in Cayenne have the same power
as predicate logic, so you can specify most anything you like.
Here's a poss
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> [Fergus wrote:]
> > The basic problem that I have with this is that although dependent types
> > do allow you to specify a lot of things in the type system, I'm not sure
> > that using the ty
Sat Feb 20 1999, Nick Kallen ->
: > sort :: (l :: [a]) -> ComplicatedTypeToSpecifySorting l
: >
: > Well, here's an implementation:
: >
: > sort xs = sort xs
: >
: > It's type correct, but doesn't really do what you want.
:
: What if you do this:
:
: sort (x:xs) = sort elts_lt_x ++ sort elts
[EMAIL PROTECTED] writes:
> enabling types to express all properties you want is, IMO, the right way.
Why do I feel that there must be another approach to programming?
How many people do you expect to program in Haskell once you are done adding all
it takes to "express all imaginable properties
> > > F a * = member (map (F a) [0..]) // member [a] a -> Bool
> > I mave no clue what this means. What is `member'?
>
> Member is memq, in, etc. Checks for membership in a list.
I'm still lost. What is // and how does it bind?
This is how I parse it:
(member (map (F a) [0..])) // ( (member
1 - 100 of 131 matches
Mail list logo
