gmane.comp.lang.haskell.prime

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton-Jones — 2012-05-24T14:24:45

See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
(as yet unimplemented)

Simon

| -----Original Message-----
| From: haskell-prime-bounces-HC+Z4NTRIlBAfugRpC6u6w< at >public.gmane.org [mailto:haskell-prime-
| bounces-HC+Z4NTRIlBAfugRpC6u6w< at >public.gmane.org] On Behalf Of AntC
| Sent: 24 May 2012 14:00
| To: haskell-prime-HC+Z4NTRIlBAfugRpC6u6w< at >public.gmane.org
| Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level
| recursion
| 
|  <oleg< at >...> 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:
| >
| > http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
| >
| I have now worked through that post in detail, thank you. And replied
| (on the cafe http://www.haskell.org/pipermail/haskell-cafe/2012-
| May/101417.html )
| 
| As

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC — 2012-05-24T13:00:19

I have now worked through that post in detail, thank you. And replied (on the 
cafe http://www.haskell.org/pipermail/haskell-cafe/2012-May/101417.html )

As SPJ says there, I don't expect there's any real difference in the fundeps 
approach compared to type families. And as a matter of taste, I find type 
families more easy to understand and reason about, and more *functional*.

But I don't see in SPJ's post any real doubts about soundness, just 
restrictions that would have to be imposed. He concludes "I believe that 
if ..., then overlap of type families would be fine."

The only onerous restriction is that overlapping instances would have to be in 
a single module. And I don't think that is needed under my proposal to dis-
overlap overlaps.

As a matter of interest, how would the TTypeable approach address those 
examples? Particularly the existentials (examples 3 and 4). How would it look 
inside the GADTs to discharge the constraints (or apply the type functions)?

I notice example 4 (and 1) 'exploits'

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC — 2012-05-24T00:37:56


Thanks Oleg. I'm familiar with that style from HList, but it still seems 
cumbersome to me (compared to separate equations). I suppose a type-level if-
then-else would be possible? Does this read any better?

    type instance F x = IF (EQ (TYPEOF x) INT) Bool [x]

I note there by the way, that INT ~ (TYPEOF Int), is that upshifting the name 
going to work well for all Prelude types?
    How about (TYPEOF ()) or (TYPEOF [a])?
The EQ seems somehow redundant. We can only test type (reps) for equality, or 
do you envisage inducing some ordering over typereps?

How scalable is your approach with multi-argument type functions? Such as:

    module Mine where
      type family F a b

      data Mine = ...
      type instance F Mine Int = ...
      type instance F Mine y   = ...          -- overlap on 2nd arg

    module Yours where
      import Mine

      data Yours = ...
      type instance F Yours Bool = ...         -- no overlap with F Mine b
      type instance F Yours y   = ...          -- overlap on 2nd a

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC — 2012-05-23T10:55:31

for things they'd like GHC to do?  

The two things are, I think, trying to achieve the same objective. Namely, 
supporting type-level inference driven from a type-level equality predicate.

Of those two things (details continued below), I understand Oleg does have a 
concrete proposal for the first (and a prototype). My proposal earlier in the 
thread was along the lines of your second particular thing. But I delayed 
replying immediately:
- Oleg suggested I refer back to several similar threads in July 2010
        (thank you, that was indeed a valuable discussion)
- GHC has now delivered robust type inference with type equality constraints,
- and superclass constraints.
- And we have the beginnings of data Kinds
- And there has been 'loose talk' of closed Kinds

(To explain that last: I believe the type inference for closed Kinds will need 
a similar mechanism to overlapping instances for TypeFamilies.)

Although this thread is titled FunctionalDependencies, I'm not going to say 
anything about them exce

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC — 2012-05-22T23:47:31


Yikes! I'd better post the code. This assumes all the usual HList 
infrastructure, especially class/method TypeCast as defined in-line per  
http://okmij.org/ftp/Haskell/typecast.html

Works on Hugs version Sep 2006 -- yes! it's been hiding in plain view all 
these years.

{- hDeleteMany does a type-indexed scan through an HList,
        removing all elements type `e`, even if they occur many times.
        Takes the standard HList idiom of 3 instances:
        - end of HList -- contains only HNil
        - HList's head contains the element of interest (HCons e l'')
        - HList's head not interesting, pass on (HCons e' l'')
        The 'interesting' instance overlaps the 'not interesting'.
-}

    class HDeleteMany e l l'where-- no fundep
        hDeleteMany:: e -> l -> l'

    instance (TypeCast HNil l') => HDeleteMany e HNil l'where
        hDeleteMany e HNil= typeCast HNil
                           -- must typeCast the result

    instance (HDeleteMany e l'' l') => HDeleteMany e (HCons e l'

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC — 2012-05-22T10:13:06

Hi Oleg, I appreciate it's been a very long time since this thread was active. 
But I think I might have discovered that you and Ralf were premature to reject 
overlaps w.r.t. HList.

The headline news is that I have implemented hDeleteMany in Hugs.

I'm dragging up this ancient history not to argue in favour of fundeps, nor to 
bring Hugs back from its slumbers, but pro a better-implemented approach to 
overlaps (preferably available with Type Families).

To recap the context:

Also the original post said:

The point at which the HList paper "give up on persuading Hugs" was with the 
instance definitions for hDeleteMany [Section 6 'Ended up in murky water'] 
because "There is no real consensus on the overlapping instance mechanism as 
soon as functional dependencies are involved. ... Hugs reports that the 
instances are inconsistent with the functional dependency for HDeleteMany."

There has been a lot of water under the bridge since that interchange. In 
particular, GHC has got type equality constraints m

Re: Creating a list of extensions to add to Haskell'

Freddie Manners — 2012-04-19T23:10:43


I think that may be oversimplifying the issue.

For example, there are cases such as FunDeps and TypeFamilies where --
probably -- precisely one should end up in the language, but we're not sure
which -- or maybe there's some other solution yet to be found which is
better than both.

We're never going to find out which it is unless people write a lot of code
using both extensions (and that code gets onto Hackage).  However, adding
both to the standard at this stage would probably mean removing one or both
later, which causes even bigger problems.

When an extension is no longer supported,


I think there's a degree of "common knowledge" out there that some
extensions (FD's and TypeFamilies included) are here for
the foreseeable future -- i.e. they're pretty stable and certainly the
compiler isn't going to forget about them soon.  Others are maybe more
experimental or obsolete.  I agree that if that information isn't clearly
written down somewhere, it should be.

Packages, using rejected extensions, should

Creating a list of extensions to add to Haskell'

Henk-Jan van Tuyl — 2012-04-19T21:50:54

L.S.,

Many libraries on Hackage use language extensions, or depend on other
libraries that use extensions. When an extension is no longer supported,
or another Haskell compiler must be used,
this may lead to a lot of maintenance work.

To prevent an extreme amount of maintenance, I try to avoid using language
extensions, but many libraries on Hackage use them.

My proposal is:
Make an inventory, of the most used language extensions (based
on the number of Hackage downloads of packages depending directly or
indirectly on them).  If the most used extensions are theoretically sound
and improve software developed with them, they should be included in the
next Haskell standard.

Packages, using rejected extensions, should be redesigned or shunned
(marked as such in Hackage).

Regards,
Henk-Jan van Tuyl

Re: String != [Char]

Greg Weber — 2012-04-01T15:22:32

I am starting up the proposal.

http://hackage.haskell.org/trac/haskell-prime/ticket/143
http://hackage.haskell.org/trac/haskell-prime/wiki/OpaqueText

Unfortunately I haven't had any time to work on this for the last week
and won't for 2 more weeks.
Your help is appreciated. I think the first step is to move list
functions into a separate module for the Text package to see if we can
get rid of name conflicts with the Prelude.

On Sat, Mar 31, 2012 at 11:49 PM, Colin Paul Adams
<colin-vnRo6g/zHhuHCRyBVyKX4rVCufUGDwFn< at >public.gmane.org> wrote:

Re: String != [Char]

Colin Paul Adams — 2012-04-01T06:49:11

    Gabriel> On Mon, Mar 26, 2012 at 5:08 AM, Christian Siefkes

    Gabriel> It is not the precision of Char or char that is the issue
    Gabriel> here.  It has been clarified at several points that Char is
    Gabriel> not a Unicode character, but a Unicode code point. 

That's not what the standard says:

6.1.2 Characters and Strings

The character type Char is an enumeration whose values represent Unicode
characters [2]. 

[2]   Unicode Consortium. Unicode
standard. http://unicode.org/standard/standard.html.

Faça parte da minha rede no LinkedIn

Carlos Camarao Figueiredo — 2012-03-29T18:02:06

LinkedIn
------------



Eu gostaria de adicioná-lo à minha rede profissional no LinkedIn.
-Carlos Camarao

Carlos Camarao Figueiredo
Professor na UFMG
Belo Horizonte e Região, Brasil

Confirme que você conhece Carlos Camarao Figueiredo:
https://www.linkedin.com/e/g4afbk-h0e41yt6-n/isd/6485083729/t-WWDysg/?hs=false&tok=1Rt6jCLOCW0Bc1

--
Você está recebendo convites de conexão por e-mail. Clique aqui para parar de recebê-los:
http://www.linkedin.com/e/g4afbk-h0e41yt6-n/TxW8ibFUf804HWGRSSBmLzVTlbMbbXm3PVJ5g9-/goo/haskell-prime%40haskell%2Eorg/20061/I2249830483_1/?hs=false&tok=1uXcs9Xx6W0Bc1

(c) 2012 LinkedIn Corporation. 2029 Stierlin Ct, Mountain View, CA 94043 - EUA.

_______________________________________________
Haskell-prime mailing list
Haskell-prime-HC+Z4NTRIlBAfugRpC6u6w< at >public.gmane.org
http://www.haskell.org/mailman/listinfo/haskell-prime

Re: String != [Char]

Yitzchak Gale — 2012-03-27T19:27:34

For the record, I have a more fundamental objection to
OverloadedStrings. When library authors write partial functions
for the fromString method - and we see in practice that
they do so - it creates the shocking situation in which
invalid syntax of a literal is only caught at run time.

Instead, Haskell' should provide a pragma, or other
syntactic mechanism, by which compilers can allow
specific types other than String for string literals at
*compile* time in a monomorphic context. The
implementation of that syntax would be compiler
dependent, of course. For GHC, Template Haskell
could help. Another approach would be for a
compiler to have a built-in way of embedding, say,
Text literals directly in object code.

For people who like OverloadedStrings despite this
problem, it could be available via a pragma. But
never by default - it should be possible to get
fundamental string types like Text and ByteString
for string literals without having to turn on
OverloadedStrings. In GHC, quasi-quoters are the
right w

Re: String != [Char]

Evan Laforge — 2012-03-27T01:40:46

Definitely, I have ones that would need some :: sprinkled in.


Also me :)  I'd like that 'default' keyword back too, it's too useful
for variables names to waste on something so obscure.

That said, I like OverloadedStrings.

Re: String != [Char]

Edward Kmett — 2012-03-26T22:19:59


Agreed. Haskell-prime has in the past gone out of its way not to
standardize anything that hasn't actually been implemented somewhere.



I would agree that OverloadedStrings definitely needs to work with
defaulting better! I've been bitted by this in my own code.

In the past I have longed for a trivial class

class Defaulting a

which merely served to meet the conditions for extended default from

http://www.haskell.org/ghc/docs/6.6/html/users_guide/ch03s04.html#extended-default-rules
*
*



by adding Defaulting to the list of extra classes the language permits.

In the special case of ghc where we have polymorphic kinds now, the
Defaulting class could allow for defaulting  rules to then be applied
trivially for higher kinds, and when you have new classes you really want
defaulting to apply, like in this case IsString, you could just add
Defaulting as a superclass constraint.

A passing thought: nearly anything can be made an instance of


I don't like the idea of adding a toString to IsString. One of th

Re: String != [Char]

Ben Millwood — 2012-03-26T21:56:58

Does this mean we've firmly established that there currently is *no*
completely satisfactory method of dealing with Unicode in existence
today? In that case, even if it /will be/ a good idea one day, can't
we agree that it's not the right time to deprecate String = [Char]?
The language has a good history, I understand, of not standardising
that which is not implemented and in common use, so if we'd like to
change Text before introducing it to the language, I say let's do that
separately.

No-one's yet argued against OverloadedStrings. I think there /is/ an
argument to be made, that it introduces ambiguity and could break
existing programs (probably we can extend defaulting to take care of
this, but I think there are people who'd be happier if we killed
defaulting too). Too much polymorphism /can/ be a bad thing. But I
think there's a serious chance we can make that happen, and make Text
a bit more pleasant to work with.

A passing thought: nearly anything can be made an instance of
IsString, via something r

Re: String != [Char]

David Menendez — 2012-03-26T20:24:20

On Mon, Mar 26, 2012 at 1:12 PM, Christian Siefkes
<christian< at >siefkes.net> wrote:

Unicode contains a set of precomposed characters, like ö, that can be
normalized to a single code point, but this is not true of every
combination of characters.

Prelude> "ā́"
"a\772\769"

As far as I know, there is no representation of ā́ which uses a single
code point.

Re: String != [Char]

Gabriel Dos Reis — 2012-03-26T17:36:52

On Mon, Mar 26, 2012 at 11:42 AM, Christian Siefkes
<christian-0a8dUXqrJ1fR7s880joybQ< at >public.gmane.org> wrote:


The correctness problems isn't that a list is used to represent a sequence.
The problem is that that representational detail (and I agree with you
it is an implementation of sequence) is made part of the API on strings.

Re: String != [Char]

Greg Weber — 2012-03-26T17:26:11

Can the unicode experts here propose a Text API whose functions work
for all Unicode (start by removing list functions)? If there is such a
satisfactory API and it does not conflict with the Prelude we could
use it unqualified.

On Mon, Mar 26, 2012 at 10:21 AM, Johan Tibell <johan.tibell-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org> wrote:

Re: String != [Char]

Brandon Allbery — 2012-03-26T17:23:30


I think we established earlier that the list-like operations on Text are a
backward compatibility wart.  Either they should go away, or they should be
modified to operate on some other level than codepoints.  Probably the way
the ecosystem should work is that [Char] (or possibly a packed version
thereof, sort of like lazy ByteStrings with Word32 instead of Word8 as the
fundamental unit) is the codepoint view and Text is the grapheme view; both
are necessary at various times, but the grapheme view is the more natural
one for text /per se/.

Re: String != [Char]

Johan Tibell — 2012-03-26T17:21:08

We already covered this. Text inherited a list-based API, even if that
sometimes doesn't make sense.

To work with Unicode you need more specific functions for different
tasks. Text only implements a few so far, like case conversion and
case-less comparison, and asks you to use text-icu for the rest.

Re: String != [Char]

Brandon Allbery — 2012-03-26T17:21:26


I think we established earlier that the list-like operations on Text are a
backward compatibility wart.  Either they should go away, or they should be
modified to operate on some other level than codepoints.  Probably the way
the ecosystem should work is that [Char] (or possibly a packed version
thereof, sort of like lazy ByteStrings with Word32 instead of Word8 as the
fundamental unit) is the codepoint view and Text is the grapheme view; both
are necessary at various times, but the grapheme view is the more natural
one for text /per se/.