RE: Language extension proposal

[C T McBride]

Hi

> There's nothing wrong with this in principle; the difficulty is that
> when you say
>
>   mantissa + 4
>
> you aren't saying which float type to get the mantissa of.  Earlier
> messages have outlined workarounds, but in some ways the "real" solution
> is to provide a syntax for type application.  A polymorphic function
> should be applied to a type argument; these type arguments are always
> implicit in Haskell, but are explicit in System F.

You're quite right. I'd argue that instance derivations are also implicit
arguments (they're a bit like elements of a datatype family). I'd further
argue that it should never be compulsory to keep something implicit. It
should always be possible to explain to the stupid machine exactly what
you want.

> If we could only figure out a good syntax for
> (optional) type application, it would deal rather nicely with many of
> these cases.  Trouble is, '<..>' gets confused with comparisons.  And
> when there are multiple foralls, it's not obvious what order to supply
> the type parameters.

It's as obvious (or not) as remembering the order of arguments expected by
any function, and in a dependently-typed language it's exactly that. My
counsel would be to make Haskell's type-level programming language follow
the functional idiom as much as is practicable. If you think of it as not
so much extending Haskell's type system, but as grabbing for Haskell a
bigger slice of a richer theory, the obvious question is `why stop now?'.
Syntactically, it'd be prudent to ensure that what's chosen for this
extension doesn't make the next extension uglier or more difficult.

The approach we take to implicit syntax in Epigram is a small variation
on Pollack's system from the early nineties. It goes like this

(1) We have a postfix operator _ (pronounced `sub' for `subscript') which
  means `make the first argument explicit'; it also prefixes the
  variable in a quantifier to indicate that the argument is implicit
  by default; functions with implicit arguments are by default
  applied to unknowns

  e.g.  nil  :  all _ x : * . List x

  sonil  means  nil applied to an unknown x
nil _means  nil unapplied (thus still `polymorphic')
nil _ X  means  nil explicitly applied to X

(2) We have a symbol ? which means `I don't know or care what goes here',
  used to make the machine try to figure out an explicit argument.

  so   nil _ ?  also means  nil applied to an unknown x

  By convention  f ___ x  is short for  f _ ? _ ? _ x  and so on,
  making it relatively easy to pick out specific arguments to make
  explicit.

In Haskell, I suppose that type arguments in forall situations would be
implicit by default, and type arguments to higher kind symbols would be
explicit by default, so you probably don't need to mark up the binders at
declaration time. However, I reckon the sub operator is a useful one. Note
that it's not `type application' but rather `making polymorphism
explicit', allowing the distinction between polymorphic objects and their
instances to be made precisely, an issue kind of fudged in the current
Haskell presentation of higher-rank polymorphism. Type application is a
useful by-product.

> It'd be useful in other situations too.  For example, one could have
> lambdas at the type level, if one was willing to instantiate them
> explicitly.
>   sequence :: forall (m:*->*) (a:*).  [m a] -> m [a]
>   data STB a s = s -> (a,s)   -- Oops: got the
> parameters backwards
>
>   sequence<\b. ST b MyState, Int>...

Quite so. This sort of thing happens all the time, e.g. when you have

  data Tree node leaf
 = Leaf leaf
 | Node (Tree node leaf) node (Tree node leaf)

You might well want to fmap an operation across the node data, but oh dear
it's not the last argument of the type constructor. You might also want
to fmap across all the x's in a Tree (f x) (g x). It's no big deal to
figure out the code for the fmap instance given the lambda abstraction.

Even more useful is the construction of abstractions which just weren't
there before.

  data Term = Var String | ...

Suppose I forgot to make my representation polymorphic in variable names.
(Or suppose I have too many interesting substructures to be able to
abstract them all at once.) I should be able to express Term as something
like

 (\ string . data Term = Var string | ... ) String
   -- categorists may read data Term = ... | ... as mu Term . ... + ...

and still get fmap (renaming) built for me. Indeed that particular idiom
could well be so handy that it deserves an even shorter syntax like

 (Term \\ String)

As with any functional programming language, strength comes from the
ability to express useful abstractions. The type level is no different
to the term level in this respect.

Cheers

Conor


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/list

Re: Language extension proposal

[Ashley Yakeley]

At 2003-06-30 01:55, Ralf Hinze wrote:

>What about 
>   mantissa (| Double |) + 4 ?

This would work perfectly with my method if (| Double |) were syntactic 
sugar for (mkType :: Type Double) or similar. I really think it's the 
most straightforward way of doing it and I hazard the easiest to 
implement.

-- 
Ashley Yakeley, Seattle WA
Almost empty page: 

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Language extension proposal

[Ralf Hinze]

> If we could only figure out a good syntax for
> (optional) type application, it would deal rather nicely with many of
> these cases.  Trouble is, '<..>' gets confused with comparisons.  And
> when there are multiple foralls, it's not obvious what order to supply
> the type parameters.

What about 
mantissa (| Double |) + 4 ?
Order: left to right as they appear in the quantifier or else (more
heavy-weight) several special brackets (curried foralls)
... sequence (| \ b . ST b MyState |) (| Int |) ...
So we can write
... sequence ...all foralls are implicit
... sequence (| \ b . ST b MyState |) ...   the second forall is implicit
but not
... sequence (| Int |) ...  the first forall is implicit

Cheers, Ralf

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Language extension proposal

[Simon Peyton-Jones]

If you have a class like this

class FloatTraits a where
  mantissa :: Int

then the type of mantissa is

mantissa :: forall a. FloatTraits a => Int

There's nothing wrong with this in principle; the difficulty is that
when you say

mantissa + 4

you aren't saying which float type to get the mantissa of.  Earlier
messages have outlined workarounds, but in some ways the "real" solution
is to provide a syntax for type application.  A polymorphic function
should be applied to a type argument; these type arguments are always
implicit in Haskell, but are explicit in System F.  They are also
explicit in O-O languages that support polymorphism.  For example, in
C++ one might say
mantissa + 4
And in fact that's just what we *want* to say here.  (The workarounds in
earlier emails all amount to passing a *value* argument as a proxy for a
type argument.)  If we could only figure out a good syntax for
(optional) type application, it would deal rather nicely with many of
these cases.  Trouble is, '<..>' gets confused with comparisons.  And
when there are multiple foralls, it's not obvious what order to supply
the type parameters.

It'd be useful in other situations too.  For example, one could have
lambdas at the type level, if one was willing to instantiate them
explicitly.
sequence :: forall (m:*->*) (a:*).  [m a] -> m [a]
data STB a s = s -> (a,s)   -- Oops: got the
parameters backwards

sequence<\b. ST b MyState, Int>...

Simon

| -Original Message-
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
Behalf Of Ashley Yakeley
| Sent: 28 June 2003 00:25
| To: [EMAIL PROTECTED]
| Subject: Re: Language extension proposal
| 
| In article <[EMAIL PROTECTED]>,
|  Andrew J Bromage <[EMAIL PROTECTED]> wrote:
| 
| > Another example is floating point format information, like the
| > information in C's .  One might implement this as:
| >
| > class (Bounded a) => FloatTraits a where
| > epsilon :: a-- OK
| > mantissaDigits :: Int   -- Not OK!
| 
| Oh I do this all the time in HBase. I simply do this:
| 
|  data Type a = MkType
| 
|  getType :: a -> Type a
|  getType _ = MkType
| 
|  class (Bounded a) => FloatTraits a where
|epsilon :: a
|mantissaDigits :: Type a -> Int
| 
| The only annoyance is that you frequently have to write (MkType ::
Type
| MyFloat). Syntactic sugar for _that_ would be useful.
| 
| --
| Ashley Yakeley, Seattle WA
| 
| ___
| Haskell mailing list
| [EMAIL PROTECTED]
| http://www.haskell.org/mailman/listinfo/haskell


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Language extension proposal

[Ralf Laemmel]

Ashley Yakeley wrote:
> 
> At 2003-06-28 02:51, Ralf Laemmel wrote:
> 
> >Suffering from persecution mania,
> >I prefer to know for sure that nobody never ever will
> >pattern match on those a's. So I prefer to write:
> 
> I don't understand. Did you mean pattern-match on MkType? I could stop
> that by hiding it but exposing mkType = MkType.

You are right.
My comments attack the Data.Dynamic.typeOf style.
Your use of a designated phantom datatype "Type" and
my use of "->" for this purpose seem to be equivalent.

Ralf
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Language extension proposal

[Ashley Yakeley]

At 2003-06-28 02:51, Ralf Laemmel wrote:

>Suffering from persecution mania,
>I prefer to know for sure that nobody never ever will 
>pattern match on those a's. So I prefer to write:

I don't understand. Did you mean pattern-match on MkType? I could stop 
that by hiding it but exposing mkType = MkType.


-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Language extension proposal

[Ralf Laemmel]

Ashley Yakeley wrote:

> Oh I do this all the time in HBase. I simply do this:
> 
>  data Type a = MkType
> 
>  getType :: a -> Type a
>  getType _ = MkType
> 
>  class (Bounded a) => FloatTraits a where
>epsilon :: a
>mantissaDigits :: Type a -> Int

Suffering from persecution mania,
I prefer to know for sure that nobody never ever will 
pattern match on those a's. So I prefer to write:


-- Values serving as type arguments
type TypeArg a = a -> ()

-- Constant function as type argument
typeArg :: TypeArg a
typeArg = const ()

-- Extract type argument from value
getTypeArg :: a -> TypeArg a 
getTypeArg _ = typeArg


I start to use this style more agressively in Strafunski
and the boilerplate gmaps. 

A side remark: Data.Dynamic does NOT use this style but rather
Ashley's:

...
typeOf :: a -> TypeRep
...

which is a pitty because there is nothing in the type which
prevents you from looking at a; its only in the comments.
Every now and then I get this wrong.
 
> The only annoyance is that you frequently have to write (MkType :: Type
> MyFloat). Syntactic sugar for _that_ would be useful.

On the other hand, supporting the above style with TypeArg's 
by an ADT, would make the whole thing entirely safe and transparent.


-- 
Ralf Laemmel
VU & CWI, Amsterdam, The Netherlands
http://www.cs.vu.nl/~ralf/
http://www.cwi.nl/~ralf/
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Language extension proposal

[Ashley Yakeley]

In article <[EMAIL PROTECTED]>,
 Andrew J Bromage <[EMAIL PROTECTED]> wrote:

> Another example is floating point format information, like the
> information in C's .  One might implement this as:
> 
>   class (Bounded a) => FloatTraits a where
>   epsilon :: a-- OK
>   mantissaDigits :: Int   -- Not OK!

Oh I do this all the time in HBase. I simply do this:

 data Type a = MkType

 getType :: a -> Type a
 getType _ = MkType

 class (Bounded a) => FloatTraits a where
   epsilon :: a
   mantissaDigits :: Type a -> Int

The only annoyance is that you frequently have to write (MkType :: Type 
MyFloat). Syntactic sugar for _that_ would be useful.

-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Language extension proposal

[Andrew J Bromage]

G'day all.

On Wed, Jun 25, 2003 at 08:48:12AM -0700, Hal Daume wrote:

> I'm not sure this is really necessary (at least syntax-wise).

Well, of course, no extension is absolutely necessary in a Turing-hard
language. :-)

For the record, here are a couple of other solutions which avoid the
problem.  You could, for example, make the return type a phantom
type:

newtype T a = T Int

class Trait a where { trait :: T a }

instance Trait Int  where { trait = T 0 }
instance Trait Char where { trait = T 1 }

Or construct the type dictionary explicitly:

data Traits a
= Traits {
trait1 :: a,
trait2 :: Int
  }

class Trait a where
traits :: Traits a

instance Trait Char where
traits = Traits {
trait1 = 'a',
trait2 = 16
 }

Neither solution seems as nice, though, particularly as the traits
typeclass idiom is already entrenched (e.g. Bounded).

> As far as I can tell with the various --ddump-* flags, the compiler
> hasn't yet figured out that the argument to trait is useless (i.e., it
> keeps it in there).

Nor can it, because you could easily declare an instance in another
module for which the argument is _not_ useless.  This is impossible to
detect at compile time.

> Of course, the powers that be can weight in on this, and I'm sure that
> you're aware of the phantom type solution, but I figured I'd post anyway
> so that others can get a look at types like this for their own
> benefit...

Sure.  Any input is good.  I'm not convinced that my proposed solution
is the best one.  (I'm pretty sure that it's the minimal extension
required, though.)

Cheers,
Andrew Bromage
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Language extension proposal

[Hal Daume]

I'm not sure this is really necessary (at least syntax-wise).

We can do something like:

> data T a
> class Trait a where { trait :: T a -> Int }
> 
> instance Trait Int  where { trait _ = 0 }
> instance Trait Char where { trait _ = 1 }

As far as I can tell with the various --ddump-* flags, the compiler
hasn't yet figured out that the argument to trait is useless (i.e., it
keeps it in there).

However, from a sanity point of view, I much prefer to write my "useless
arguments" like this; that way at least *I* know that they'll never be
evaluated.  I suppose the only thing that could go wrong is someone
writing:

> instance Foo Bool where { trait x = x `seq` 1 }

in which case it would be wrong for the compiler to get rid of this
argument.

I suppose that your solution gets rid of this problem by relizing that
seq doesn't have absent demand on its argument (quite the opposite, in
fact).

Of course, the powers that be can weight in on this, and I'm sure that
you're aware of the phantom type solution, but I figured I'd post anyway
so that others can get a look at types like this for their own
benefit...

--
 Hal Daume III   | [EMAIL PROTECTED]
 "Arrest this man, he talks in maths."   | www.isi.edu/~hdaume


> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of Andrew J Bromage
> Sent: Tuesday, June 24, 2003 9:18 PM
> To: [EMAIL PROTECTED]
> Subject: Language extension proposal
> 
> 
> G'day all.
> 
> I've been toying with an idea for a small language extension, and I
> was curious what you all think of this.
> 
> As a motivating example, consider the following standard typeclass:
> 
>   class Bounded a where
>   min :: a
>   max :: a
> 
> This is an example of what I refer to as a "traits typeclass" (by
> analogy to traits classes, well-known to C++ programmers).  The idea
> is that you want to specify certain properties/operations which depend
> on a _type_, rather than any particular value of that type.
> 
> Another example is floating point format information, like the
> information in C's .  One might implement this as:
> 
>   class (Bounded a) => FloatTraits a where
>   epsilon :: a-- OK
>   mantissaDigits :: Int   -- Not OK!
> 
> For obvious reasons, the declaration of mantissaDigits is not valid
> Haskell.  Instead, you might do something like this:
> 
>   class FloatTraits a where
>   mantissaDigits :: a -> Int
> 
>   instance FloatTraits Float where
>   mantissaDigits _ = 24
> 
>   instance FloatTraits Double where
>   mantissaDigits _ = 53
> 
> and invoke it as, say:
> 
>   mantissaDigits (undefined :: Float)
> 
> A decent strictness analyser can tell if an argument to some function
> is always unused (in GHC core terminology, this means its demand is
> "absent") and thus avoid passing the argument at all.  However, it is
> currently impossible to tell if this is true all instances of a
> typeclass.  What I would like is some annotation that I can 
> use to tell
> my compiler that this argument of this method is always unused, no
> matter what instance it resolves to.
> 
> My proposal is to grab a new punctuation symbol (I will use '~' as
> an example) to sit alongside the GHC extension use of '!'.  Where '!'
> means that an argument may be evaluated before calling a function, '~'
> means than an argument may be ignored by the callee.  So in the above
> example, I can write:
> 
>   class FloatTraits a where
>   mantissaDigits :: ~a -> Int
> 
> Now this marker is not as simple to implement as '!'.  The strict
> marker is advisory; if you stripped all '!'s from your program, it
> would still have the same static semantics.  Not so with '~', which
> must be statically checked.
> 
> However, the static analysis is pretty trivial, except for the
> problem of inference.  Basically, if a variable has absent demand,
> it a) can't be pattern matched on (unless the pattern is a variable,
> of course), and b) can't be passed as an argument to a function
> (including a data constructor) which doesn't also treat that argument
> as having absent demand.
> 
> I therefore propose that the marker not be inferred for top-level
> definitions, or at least for exported definitions.  If you declare it,
> it's checked, but otherwise it's not.  In addition, any calls that you
> pass a variable with absent demand to must themselves have the marker
> declared explicitly in thei

Language extension proposal

[Andrew J Bromage]

G'day all.

I've been toying with an idea for a small language extension, and I
was curious what you all think of this.

As a motivating example, consider the following standard typeclass:

class Bounded a where
min :: a
max :: a

This is an example of what I refer to as a "traits typeclass" (by
analogy to traits classes, well-known to C++ programmers).  The idea
is that you want to specify certain properties/operations which depend
on a _type_, rather than any particular value of that type.

Another example is floating point format information, like the
information in C's .  One might implement this as:

class (Bounded a) => FloatTraits a where
epsilon :: a-- OK
mantissaDigits :: Int   -- Not OK!

For obvious reasons, the declaration of mantissaDigits is not valid
Haskell.  Instead, you might do something like this:

class FloatTraits a where
mantissaDigits :: a -> Int

instance FloatTraits Float where
mantissaDigits _ = 24

instance FloatTraits Double where
mantissaDigits _ = 53

and invoke it as, say:

mantissaDigits (undefined :: Float)

A decent strictness analyser can tell if an argument to some function
is always unused (in GHC core terminology, this means its demand is
"absent") and thus avoid passing the argument at all.  However, it is
currently impossible to tell if this is true all instances of a
typeclass.  What I would like is some annotation that I can use to tell
my compiler that this argument of this method is always unused, no
matter what instance it resolves to.

My proposal is to grab a new punctuation symbol (I will use '~' as
an example) to sit alongside the GHC extension use of '!'.  Where '!'
means that an argument may be evaluated before calling a function, '~'
means than an argument may be ignored by the callee.  So in the above
example, I can write:

class FloatTraits a where
mantissaDigits :: ~a -> Int

Now this marker is not as simple to implement as '!'.  The strict
marker is advisory; if you stripped all '!'s from your program, it
would still have the same static semantics.  Not so with '~', which
must be statically checked.

However, the static analysis is pretty trivial, except for the
problem of inference.  Basically, if a variable has absent demand,
it a) can't be pattern matched on (unless the pattern is a variable,
of course), and b) can't be passed as an argument to a function
(including a data constructor) which doesn't also treat that argument
as having absent demand.

I therefore propose that the marker not be inferred for top-level
definitions, or at least for exported definitions.  If you declare it,
it's checked, but otherwise it's not.  In addition, any calls that you
pass a variable with absent demand to must themselves have the marker
declared explicitly in their type signatures.

There may also be an argument for extending '~' to data constructors,
in the same way that H98 uses '!'.  This would allow parameters with
absent demand to be stored in data structures.  I can't think of a
use for this right now, but it shouldn't be too much harder to add.

What do you all think?  Useful?  Not worth the effort?

Cheers,
Andrew Bromage
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

language extension proposal

[S.D.Mechveliani]

Dear Haskell users and developers,

I announce that  manual.txt  from the archive

   ftp.botik.ru:/pub/local/Mechveliani/docon/2/docon-2.zip
http://www.botik.ru...
 
contains the section 
--
 {lne} Language extension proposal
 *

Adding the following language features seem to make Haskell more fit
the needs of programming mathematics:

  (der)more "deriving" abilities
  (overl)  extended polymorphism for values and instance overlap
  (dc) automatic conversion between types (domains)
  (recat)  reorganising standard algebraic categories
  (es) equational simplifier annotations
...
...
--

You see, i worry about Haskell fitness for the programming of certain 
tasks.


--
Sergey Mechveliani
[EMAIL PROTECTED]