ould use (++) instead
>> of (<>) in this conversation just yet, but I want to clear a few things up.
>>
>> One of the early options when the operator (<>) was coined was to try to
>> say we should just generalize the type of (++) instead to make it mappend.
>&g
, but I want to clear a few things up.
>
> One of the early options when the operator (<>) was coined was to try to
> say we should just generalize the type of (++) instead to make it mappend.
> (Note: it originally was mplus, in a Haskell version long long ago, so it
> kee
Note: I realize nobody is directly saying that we should use (++) instead
of (<>) in this conversation just yet, but I want to clear a few things up.
One of the early options when the operator (<>) was coined was to try to
say we should just generalize the type of (++) instead to mak
Vassil Ognyanov Keremidchiev wrote:
> What do you think of making (++) the same as (<>) so we could use ++ as
> concatenation of any monoid, not just lists in Haskell 2020?
> This will be more intuitive for beginners, too.
Two symbolic operators that are synonymous seems a bit of a waste. I
Do you really mean at the type level?
On 3 Jul 2017 12:11 pm, "Vassil Ognyanov Keremidchiev" <var...@gmail.com>
wrote:
> Hello!
>
> What do you think of making (++) the same as (<>) so we could use ++ as
> concatenation of any monoid, not just lists in Haskell 2
Hello!
What do you think of making (++) the same as (<>) so we could use ++ as
concatenation of any monoid, not just lists in Haskell 2020?
This will be more intuitive for beginners, too.
Best regards,
Vassil Keremidchiev
___
Haskell-prime mailing list
type-level
| recursion
|
| Simon Peyton-Jones simonpj@... writes:
|
|
| No I didn't intend to put more in the header, perhaps less.
| I've added more clarification.
|
| Simon
|
| Thanks Simon, I agree with keeping it terse; I agree with your yuk
| rating for `of'. At risk of bikeshedding
Cc: haskell-prime@haskell.org
Subject: Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hi,
On Tue, May 29, 2012 at 11:03 AM, AntC
anthony_clay...@clear.net.nzmailto:anthony_clay...@clear.net.nz wrote:
Simon Peyton-Jones simonpj@...mailto:simonpj@... writes:
See also http
Simon Peyton-Jones simonpj@... writes:
I have expanded the draft spec on
http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
Thanks Simon, that's much clearer.
By the way, are the examples for the multi- type instance declarations quite
as intended? The heads have no head, as it were. Did
Hi,
On Tue, May 29, 2012 at 11:03 AM, AntC anthony_clay...@clear.net.nz wrote:
Simon Peyton-Jones simonpj@... writes:
See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
(as yet unimplemented)
Simon
Thank you Simon (and Pedro).
Are you inviting
oleg@... writes:
I don't think Overlapping Instances will be in Haskell' any time soon
since there are doubts about the soundness. Overlapping
instances are clearly unsound with type functions. Whether they are
sound with functional dependencies is not clear, but there are warning
signs
: TypeFamilies vs. FunctionalDependencies type-level
| recursion
|
| oleg@... writes:
|
|
|
| I don't think Overlapping Instances will be in Haskell' any time soon
| since there are doubts about the soundness. Overlapping instances are
| clearly unsound with type functions. Whether
-implemented approach to
overlaps (preferably available with Type Families).
To recap the context:
[AntC wrote]
Selecting instances based on inequalities is already implemented in
GHC and Hugs. (And has been successfully used for over a decade.)
You've used it extensively yourself
Hello,
On Tue, Aug 2, 2011 at 6:10 PM, Simon Peyton-Jones
simo...@microsoft.com wrote:
Julien: we should start a wiki page (see
http://hackage.haskell.org/trac/ghc/wiki/Commentary, and look for the link to
Type level naturals; one like that). On the wiki you should
* add a link
But you have just pushed the problem off to the definition of EQ. And
your definition of EQ requires a finite enumeration of all types, I
think. But * is open, so that's hard to do. What you want is
type instance EQ where
EQ a a = TRUE
EQ _ _ = FALSE
and now we are back
Oleg
| There seems no reason in principle to disallow
| type instance F where
|F Int = Bool
|F a = [a]
|
|
| I would implement this as follows:
|
| type instance F x = F' (EQ (TYPEOF x) INT) x
| type family F' trep x
| type instance F' TRUE x = Bool
| type instance F
| GHC trac ticket on the feature, as you probably saw. After a
| discussion with other people here at
| HacPhi, I've decided that what I'm going to attempt is to add
| type-level Maybes
Hang on! Julien Cretin (from INRIA) is doing an internship here at Cambridge
with Dimitrios and me
But BetterTypeRep is still a value-level thing. You want a type-level
type representation, for reasons I don't yet understand.
2. Support for overlapping type function equations.
I'd like to have type-level type representations to _implement_
overlapping type function equations. With type
Helllo,
On Sat, Jul 30, 2011 at 2:11 AM, o...@okmij.org wrote:
Second, what is the status of Nat kinds and other type-level data that
Conor was/is working on? Nat kinds and optimized comparison of Nat
kinds would be most welcome. Type level lists are better still
(relieving us from Goedel
By the way, I have been testing your type-nats branch this week. I
added my observations to the
GHC trac ticket on the feature, as you probably saw. After a
discussion with other people here at
HacPhi, I've decided that what I'm going to attempt is to add
type-level Maybes so that subtraction
Sorry for the late reply.
Thanks Oleg, I take it the Northern hemisphere is now on
academic summer holidays.
[snip]
Finally, I still think most of the magic in everything
we've been talking about boils down to being able to
have a type variable that can take on any type *except
my context stack (to 21 by
default). Obviously any kind of unicode encoding of type names is
going to run into the same sort of problem.
I would call this a bug, a recent one. Old versions of GHC (before
6.10, I think) imposed no context stack restrictions on programs with
decidable instances
ambitious system to support
type-safe loading. See, for example
http://www.mpi-sws.org/~rossberg/papers/Rossberg%20-%20The%20Missing%20Link.pdf
and other papers on his web page. He now works at Google, btw.
I wish I knew ML better, but from looking at that paper, I can't
figure out the key
Hi Oleg,
On Wed, Jun 22, 2011 at 09:36, o...@okmij.org wrote:
the need to define a duplicate of the class (MonadState' in your
example) bloats the code significantly.
I'm quite puzzled at the statement. Is there really significant
bloat? Let us count.
As the first example, let's take
| One thing you could do to help in this specific case would be to use a
| different M1 tag--e.g., M1 S ... for selectors and M1 NS ... for
| fields without selectors (or K1 NS). I presume you've already
| considered this and/or it's too late to make such a change. (Or to
| move the distinction
Hi Oleg,
On Tue, Jun 21, 2011 at 09:35, o...@okmij.org wrote:
I have implemented type-level TYPEREP (along with a small library for
higher-order functional programming at the type level). Overlapping
instances may indeed be avoided. The library does not use functional
dependencies either
Hi,
2011/6/21 Simon Peyton-Jones simo...@microsoft.com
| One thing you could do to help in this specific case would be to use a
| different M1 tag--e.g., M1 S ... for selectors and M1 NS ... for
| fields without selectors (or K1 NS). I presume you've already
| considered this and/or it's
At Tue, 21 Jun 2011 00:35:46 -0700 (PDT),
o...@okmij.org wrote:
I have implemented type-level TYPEREP (along with a small library for
higher-order functional programming at the type level). Overlapping
instances may indeed be avoided. The library does not use functional
dependencies
Hi all,
Concerning 2. combination with overlapping instances, you say The
solution has been described already in the HList paper: provide
something the typeOf at the type level. That is, assume a type
function TypeOf :: * - TYPEREP.
...
Incidentally Pedro's new deriving Generic
| I'd like to summarize the relationship between functional dependencies
| and type functions, and propose a solution that should get rid of
| overlapping instances. The solution does not require messing with
| System-FC. In fact, it can be implemented today (although
| ungainly). A small bit
At Fri, 17 Jun 2011 13:21:41 +,
Simon Peyton-Jones wrote:
Concerning 1. mutual dependencies I believe that equality
superclasses provide the desired expressiveness. The code may not
look quite as nice, but equality superclasses (unlike fundeps) will
play nicely with GADTs, type families
| By equality superclasses, do you just mean being able to say a ~ b
| in a class context?
Yes. Or (F a ~ b).
| Unless I'm missing something, that is not sufficient to do a lot of
| things I would like to do, as those things require both
| OverlappingInstances and FunctionalDependencies (as
| Is there a policy that only a proposal's owner can modify the wiki
| page? Or that you have to be a member of the Haskell' committee?
I'm not sure. Malcolm Wallace is chair at the moment; I'm ccing him.
I have no idea: I neither set up the wiki, nor do I have any interesting admin
| class C a b | a - b where
| foo :: a - b
| foo = error Yo dawg.
|
| instance C a b where
|
| The instance 'C a b' blatantly violates functional dependency and
| should not have been accepted. The fact that it was is a known bug in
| GHC. The bug keeps getting mentioned on
On Wed, Jun 15, 2011 at 3:25 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
Wait. What about
instance C [a] [b]
? Should that be accepted? The Coverage Condition says no, and indeed it
is rejected. But if you add -XUndecidableInstances it is accepted.
This 'clearly' violates
At Wed, 15 Jun 2011 10:36:46 +,
Simon Peyton-Jones wrote:
The issue doesn't even arise with type families:
class MonadState m where
type State m :: *
instance MonadState m = MonadState (MaybeT m) where
type State (MaybeT m) = State m
So examples
At Tue, 14 Jun 2011 19:52:00 -0700 (PDT),
o...@okmij.org wrote:
Dan Doel wrote:
class C a b | a - b where
foo :: a - b
foo = error Yo dawg.
instance C a b where
The instance 'C a b' blatantly violates functional dependency and
should not have been accepted. The
= b2)
And in fact b1 and b2 are equal, up to alpha-conversion. They are
both just free type variables.
No, this was intended to be a more semantic property. Here it is in
English:
For any three ground types a, b1, and b2, if we can prove that both C
a b1 and C a b2 hold, then b1 and b2 must
There was an interesting thread on haskell-prime [1], about the relationship
between functional dependencies and type families. This message is my attempt
to summarise the conclusions of that thread. I'm copying other interested
parties (eg Oleg, Dimitrios)
[1] http://www.haskell.org
On Tue, Jun 14, 2011 at 4:40 PM, Dan Doel dan.d...@gmail.com wrote:
On Tue, Jun 14, 2011 at 5:36 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
There was an interesting thread on haskell-prime [1], about the relationship
between functional dependencies and type families. This message
At Tue, 14 Jun 2011 09:36:41 +,
Simon Peyton-Jones wrote:
5. David wants a wiki page fixed. But which one? And how is it locked
down?
This page:
http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies
Currently under cons for FunctionalDependencies, it
into account (which is the
type class way), in which case both of the qualified instances are
illegal, because they declare instances C T b for all b (plus a
constraint on the use), which violates the fundep. I've seen examples
like this before, and I think what GHC ends up doing (now) is fixing
At Tue, 14 Jun 2011 10:40:48 -0400,
Dan Doel wrote:
1. As things stand in GHC you can do some things with functional
dependencies that you can't do with type families. The archetypical example
is type equality. We cannot write
type family Eq a b :: *
type instance Eq k
Sorry about the double send, David. I forgot to switch to reply-all in
the gmail interface.
On Tue, Jun 14, 2011 at 11:49 AM,
dm-list-haskell-pr...@scs.stanford.edu wrote:
You absolutely still can use FunctionalDependencies to determine type
equality in GHC 7. For example, I just verified
.
A functional dependency such as | a b - c d just guarantees that a
and b uniquely determine the instance. Hence, it is okay to have
class methods that do not mention type variables c and d, because the
compiler will still know which instance to pick.
Since your code only has one instance
the instance. Hence, it is okay to have
class methods that do not mention type variables c and d, because the
compiler will still know which instance to pick.
It specifies that a and b uniquely determine c and d, so the choice of
instances is unambiguous based only on a and b. This is the basis
|
http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies
|
| Currently under cons for FunctionalDependencies, it says:
|
| AssociatedTypes seem to be more promising.
|
| I proposed the following fix:
|
| AssociatedTypes seem to be more promising, but
OverlappingInstances are the only way to do recursive
programming at the type level, for the specific reasons I outlined. I
hope that before FunctionalDependencies or TypeFamilies or any other
type-level programming becomes part of Haskell', there is a way to
differentiate base and recursive
to FunctionalDependencies that I think should be there.
One of the more disgusting but also powerful implications of
FunctionalDependencies is that, in conjunction with
OverlappingInstances and UndecidableInstances, you can do recursive
programming at the type level. This has been (ab)used to do some cool
things
On 29.05.2011 22:59, David Mazieres wrote:
But now you have overlapping type synonyms, which pose a safety threat
where the more-specific instance is not in scope. Therefore, Haskell
likely cannot be extended to accept code such as the above.
No it could. Inconsistency arise from fact
at the type level. This has been (ab)used to do some cool
things (e.g., HList, HaskellDB, OOHaskell).
It would seem very strange to me if haskell-prime made the choice of
fundeps/type families based on the behaviour with
OverlappingInstances. I'm under the impression that Overlapping is
generally
On Sun, May 29, 2011 at 6:45 PM, Ben Millwood hask...@benmachine.co.uk wrote:
It would seem very strange to me if haskell-prime made the choice of
fundeps/type families based on the behaviour with
OverlappingInstances. I'm under the impression that Overlapping is
generally considered one
recursive
programming at the type level, for the specific reasons I outlined. I
hope that before FunctionalDependencies or TypeFamilies or any other
type-level programming becomes part of Haskell', there is a way to
differentiate base and recursive cases *without* overlapping
instances.
The fact
.
This seems like the only reasonable option given the meaning of
functional dependencies.
Also, in an unrelated direction: there are conditions on type families
that can allow some overlapping to be permitted. For instance, if you
simply want a closed type function, like, taking the above as an
example
Hello Evgenij,
the TDNR proposal seems related to yours:
http://hackage.haskell.org/trac/haskell-prime/wiki/TypeDirectedNameResolution
It would be useful to highlight and motivate the differences to help
others judge your proposal.
Cheers,
Sebastian
--
Underestimating the novelty of
It looks my proposal is almost a duplicate of TNDR. If I understand correctly,
TNDR still uses a global function scope with some sort of Ad-Hoc, while I
suggested that you can create a function which scope is local to a specified
type, meaning - function is in scope only
Hi,
Simon PJ wrote (Re: BangPatterns: probably accept == undecided):
Not allowing infix functions on the LHS would be a notable
simplification.
And a little later (Re: Infix type constructors):
What we *want* is to say
data a + b = Left a | Right b
That is, we want to define
| Just to clarify, issues of what names can be used for
| type constructors aside, are you proposing dropping
| infix syntax for defining functions, but retaining infix
| syntax for defining types (and type families etc.)?
|
| Or would the last example have to be written
|
| data (+) a b
Mon Apr 14 11:49:45 PDT 2008 Simon Marlow [EMAIL PROTECTED]
* add liberalised type synonyms
M ./status.hs +2
View patch online:
http://darcs.haskell.org/haskell-prime-status/_darcs/patches/20080414184945-8214f-9ef7e948faad471a9c4924002056b4fc1d3ca1fb.gz
Mon Apr 14 12:05:50 PDT 2008 Simon Marlow [EMAIL PROTECTED]
* accept scoped type variables
M ./status.hs -1 +1
View patch online:
http://darcs.haskell.org/haskell-prime-status/_darcs/patches/20080414190550-8214f-d308ff4f7fc7ca2c58b885792e45ab33c2735e77.gz
have any effect?
* on the module doing the exporting (conflict with the presence of
in-module type-signature for the same thing; type restriction in-module;
monomorphism-restriction-lifting or defaulting-removal of the named thing)
* on modules importing this one (can a module re-export something
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Arie Peterson wrote:
Isaac Dupree wrote:
One big question: can their presence have any effect?
* on the module doing the exporting (conflict with the presence of
in-module type-signature for the same thing; type restriction in-module
| I don't think you need to produce 'a=Id (Tree Int)' since that
| reduces to 'a=Tree Int'.
| In general, you don't have to produce Id applied to anything, which
| gives me some hope that it's possible to add Id and still have
| decidable (and complete) type deduction.
Yes, that's true. But I
| Ganesh and I were discussing today what would happen if one adds Id
| as a primitive type constructor. How much did you have to change the
| type checker? Presumably if you need to unify 'm a' with 'a' you now
| have to set m=Id. Do you know if you can run into higher order
| unification
.
The solutions are:
0: Int, Tree
1: Tree Int, Id
2: Id (Tree Int), Id
3: Id (Id (Tree Int)), Id
Let [EMAIL PROTECTED] denote n-ary type-level application, where T is a list of types,
and i=0. Consider the pair
( S!!(i+1), (take i S)@i)
This is the /closed-form/ for the n'th solution (m
to remove the Maybe type so I can lose all the now-redundant Just
constructors.
Well, suppose in actual fact I prefer the name CanBe to Maybe.
Then for the first part I want
type CanBe a = Maybe a
foo :: Foo CanBe
foo = ...
but of course this fails because CanBe is a non-fully-applied
Ian,
Mmm...
* Allow type Id = (I prefer this to type Id as I think we are more
likely to want to use the latter syntax for something else later
on).
Looks kind of funny; I'm not too thrilled.
* Implementations should eta-reduce all type synonyms as much as
possible, e.g.
type T
On 3/19/07, Ian Lynagh [EMAIL PROTECTED] wrote:
I'd really like to be able to define an eta-reduced Id; I see two
possibilities:
* Allow type Id = (I prefer this to type Id as I think we are more
likely to want to use the latter syntax for something else later on).
* Implementations should
Hello,
On 3/19/07, Lennart Augustsson [EMAIL PROTECTED] wrote:
Ravi,
Ganesh and I were discussing today what would happen if one adds Id
as a primitive type constructor. How much did you have to change the
type checker? Presumably if you need to unify 'm a' with 'a' you now
have to set m=Id
On Mon, Dec 11, 2006 at 12:40:33AM +0100, Twan van Laarhoven wrote:
Since operators are allowed in type and class names, I think it would
make sense if the section notation was also allowed. In particular the
Reader monad would be a little bit nicer:
instance Monad (e -) where
[still talking to myself..?]
all confluence problems in the FD-CHR paper, as far as they were
not due to instances inconsistent with the FDs, seem to be due to
conflicts between improvement and inference rules. we restore
confluence by splitting these two constraint roles, letting inference
On 3/13/06, Claus Reinke [EMAIL PROTECTED] wrote:
[still talking to myself..?]
This is all wonderful stuff! Are you perhaps planning to put it all
together into a paper?
What effect do you think this can have on existing algorithms to resolve FDs?
--
Taral [EMAIL PROTECTED]
Computer science is
for faking
dependent types? template meta-programming? a genuine type
Dynamic, as in Clean? ..). I am a bit worried that many
Haskellers appear to have given up listening here, let alone
arguing for their interests. and with the extreme timeline the
committee is insisting on, there just wont
a second oversight, in variation B: CHR rules are selected by matching,
not by unification (which is quite essential to modelling the way type
class inference works). this means that the idea of generating memo_
constraints for the instance fdis and relying on the clas fdi rules to
use
FYI, Chameleon supports a combination of lexically scoped
and partial type annotation. The latest Chameleon version
is a broken (fix on its way). Though, besides the implementation
there's also a concise formal description. See
[July 2005] Lexically Scoped Type Annotations
http
://hackage.haskell.org/trac/haskell-prime/ticket/86
- the proposal focusses on using _ as a place holder for unspecified
parts of a type or context, without discussing the alternative I'd favour:
instead of introducing holes in types and contexts to leave
parts of a declaration unspecified
I wrote:
What I don't like is that given a signature like
x :: a - a
there's no way to tell, looking at it in isolation, whether a is free or
bound in the type. [...]
Here's a completely different idea for solving this. It occurs to me that
there isn't all that much difference between
On Wed, Feb 08, 2006 at 05:48:24PM -, Simon Peyton-Jones wrote:
| b) A pattern type signature may bring into scope a skolem bound
|in the same pattern:
|data T where
| MkT :: a - (a-Int) - T
|f (MkT (x::a) f) = ...
|
|The skolem bound
On Tue, Feb 07, 2006 at 08:15:19PM +, Ben Rudiak-Gould wrote:
Simon PJ thinks that Haskell' should include scoped type variables, and I
tend to agree. But I'm unhappy with one aspect of the way they're
implemented in GHC. What I don't like is that given a signature like
x
| I think we should do the simplest thing that could possibly work,
| and then see if we really need more. By work, I mean a compatible
| extension of H98 that makes it possible to add type signatures for
| local bindings (which isn't always possible in H98). How about:
|
| * no implicit
Simon PJ thinks that Haskell' should include scoped type variables, and I
tend to agree. But I'm unhappy with one aspect of the way they're
implemented in GHC. What I don't like is that given a signature like
x :: a - a
there's no way to tell, looking at it in isolation, whether a is free
Ben Rudiak-Gould wrote:
Simon PJ thinks that Haskell' should include scoped type variables, and
I tend to agree. But I'm unhappy with one aspect of the way they're
implemented in GHC. What I don't like is that given a signature like
x :: a - a
there's no way to tell, looking
Marcin 'Qrczak' Kowalczyk [EMAIL PROTECTED] writes:
I've always liked the idea of saying 'class C' or 'type T' in
import/export lists.
Type signatures too should be allowed in export lists.
Both ideas already noted at
http://haskell.galois.com/trac/haskell-prime/wiki/ModuleSystem
Marcin 'Qrczak' Kowalczyk [EMAIL PROTECTED] writes:
Type signatures too should be allowed in export lists.
I'm all for type signatures, but I am slightly worried in that this
leads to duplication of information (giving the signature both in the
export list and at the place of definition). What
On the other hand, it is recommended
practice to define only one data type per module, isn't it?
Only by very few people as far as I know. I know that Henning
Thielemann advocates this, but it seems like a rather arbitrary
restriction to me. I find it quite common to define several data types
The Haskell Prime Wiki mentions the scoping of type variables
in class instances, but only as an aside, and it is not even clear
whether proposal 1 would support that feature or not.
For me this once occurred as a matter of language expressiveness,
i.e. I had once to switch from hugs to GHC
86 matches
Mail list logo
