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 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' separate compilation/imported
| overlapping instances to arrive at unsoundness. How does TTypeable
| handle imported instances?
| 
| AntC
| 
| 
| 
| _______________________________________________
| Haskell-prime mailing list
| Haskell-prime-HC+Z4NTRIlBAfugRpC6u6w< at >public.gmane.org
| http://www.haskell.org/mailman/listinfo/haskell-prime

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' separate compilation/imported 
overlapping instances to arrive at unsoundness. How does TTypeable handle 
imported instances?

AntC

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 arg

We'd need a clan of helper functions F'Mine, F'Yours, etc.

This multi-argument example also goes against closed type families, I think.



I can see that if we went the route of type-level Typeable, it would need 
compiler support. But do we need that? Would it be sufficient to have a 
compiler-supported if-then-else type equality? Perhaps IFEQ, like this:

    type instance F a = IFEQ a Int Bool [a]
    type instance F a = (a ?~ Int) Bool [a]     -- over-exotic syntax?

To be fair to the design you've put into TTypeable, we'd also need to handle 
polymorphic/partly-ground/higher-ranked types:

    type instance G a          = IFEQ a (Maybe b) b ()
    type instance IsFunction a = IFEQ a (_ -> _) TRUE FALSE   -- the classic
    type instance IsNum a      = IFEQ a (Num b => b) a Int

And that last example is a worry: what we're calling a type equality test is 
really a test for unifiability.

AntC

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 except that they interfere badly with overlaps, so both 
have got an unfair reputation IMHO.

Thanks to the improvements in type inference, SPJ has shown a technique he 
called "a functional-dependency-like mechanism (but using equalities) for the 
result type". That applies for Type Class instances, and GHC supports 
overlapping for those, so I've used the technique to simulate overlapping 
TypeFamily instances. 
 
difficulty with this is how to render it
pattern matching themselves.  So the FC
that would add.

I favour support for overlapping type function equations, but not exactly that 
approach. I think a major complication from the programmer's point of view is 
that the type function equations would have to be declared all in the same 
place. (I suspect there would be a similar restriction with closed Kinds.)

A complication for type inference is carrying around some representation of 
that case statement, and applying the top-to-bottom inference.

I think it preferable from a programmer's point of view to have separately 
declared stand-alone instances. And I guess this might be easier to manage for 
type inference.

And I propose a form for the instances that achieves the type function above, 
but with what you might call "explicitly non-overlapping overlaps", like this:

        type instance F Int = Bool
        type instance F a | a /~ Int = [a]  -- explicit dis-equality restraint

These can't overlap, because the restraint (aka type-level guard) says "you 
must have evidence that typevar a is not Int before this binding applies". And 
we can validate those instances for non-overlap: the instance heads overlap 
just in case a ~ Int. (I suspect much of this logic is already in place to 
handle overlapping instances. In a 2010 post Oleg gave a very convincing 
characterisation.)

[Something very similar to dis-equality guards was briefly shown in Sulzmann & 
Stuckey. A Theory of Overloading (2002).]

I'm calling these "restraints" because they're not like constraints. 
Restraints block instance matching, whereas constraints validate the instance 
_after_ matching. But the terminology is going to get confusing, because 
inside type inference, I think they'd be implemented as what's 
called "implication constraints" (as used for GADT's).

That second binding gives rise to an axiom:

        (a /~ Int ==> F a ~ [a])    -- using ==> for implication

(The axiom for the first binding is as usual, no implication needed.)


I dislike Oleg's TypeRep approach, because it brings in another layer of 
encoding. I think it would be simpler from a programmer's point of view to 
have types 'standing for themselves'.

I prefer "explicitly non-overlapping overlaps" because the type function 
guards look and behave similarly to guards for function bindings. (But a 
significant difference is that type function instances must be mutually 
exclusive, and that's how come they can be declared stand-alone. The 
requirement to be mutually exclusive means we avoid all that trouble with 
IncoherentInstances and imported overlaps silently changing behaviour -- I 
would explain further, but this post has gone on long enough.)

AntC

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'') l'  where
        hDeleteMany e (HCons _ l'')= hDeleteMany e l''

    instance (HDeleteMany e l'' l''', TypeCast (HCons e' l''') l')
         => HDeleteMany e (HCons e' l'') l'                where
            hDeleteMany e (HCons e' l'')= typeCast (HCons e' (hDeleteMany 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 mature, with powerful type 
inference. SPJ showed a technique he called "a functional-dependency-like 
mechanism (but using equalities) for the result type". [This was for an 
application where using an Associated Type would not work. So he introduced an 
extra type parameter to the class.]

I noted that HList has an approximation to equality constraints (TypeCast). I 
took the fundep away from HDeleteMany, and instead implemented the instances 
with TypeCast constraints to infer the result type:
1. There's no longer trouble with fundep interference.
2. So you can declare the instances OK (with overlaps well-ordered).
3. The typecast works a dream.

[To be precise, I haven't done away with fundeps altogether, because they 
support TypeCast. And I expect that hDeleteMany without fundeps is not going 
to play well with large-scale programs needing extensive type inference. My 
point is only that it's the interference between fundeps and overlap that 
messes up both.]

We could possibly design a better fundep, but I think fundeps are moribund. 
I'd rather put the effort into introducing overlaps into Type Families, and 
addressing the soundness concerns.


I have now studied SPJ's post, and that whole discussion. [Heck, July 2010 had 
some heavy-duty type theory.] I note that one of the threads that month was 
on 'in-equality type constraint's -- which is exactly what I think it needs to 
handle overlapping instances in a disciplined way.  SPJ's post is dense, and I 
think worth replying to in detail, now that we have mature experience with 
equality constraints.

My timing is again terrible: I suppose Northern Hemisphere academics are 
furiously ending their year and heading for the beach.

AntC

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 be redesigned or shunned

It might be useful to have a commonly used "Portability" entry on Hackage,
as in Haddock (unless there is one?). But, usually code that uses rejected
extensions will also have ceased to compile a long time ago, which you can
see in Hackage. If you have a counterexample that would help.

Regards,
Freddie

On 19 April 2012 22:50, Henk-Jan van Tuyl <hjgtuyl-/NLkJaSkS4VmR6Xm/wNWPw< at >public.gmane.org> wrote:

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

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 way to provide convenient user-defined syntax
for string-like types other than the canonical
string types.

Theoretically, polymorphism for numeric literals
is just as bad. But in practice, it seems to be much
more rare for people to implement fromIntegral
and fromRational with dangerous functions.

-Yitz

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 the more
compelling usecases is in DSLs.

Just because I can make an

instance IsString Expr where
  fromString = StringLiteral

to get a syntaxless embedding of string literals into my language for some
expression type, doesn't mean that every expression is a string literal.

Ultimately, abuses of IsString for parsing should probably just be treated
with the same general distaste as the use of Show instances that don't show
source representations.

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

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 read-like. This prospect upsets me a little :)
Maybe it would make sense to introduce additional methods, as in Num,
to make sure that some sense is maintained (perhaps toString?)

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/.