[Haskell-cafe] types calculation

Wed Nov 11 17:03:50 UTC 2015

>> If your clients will have to include fancy type-level definitions, they
will probably need UndecidableInstances. We're open to improving the
termination checker if you have a good approach to how. :)

When client wrote
> type T = T1 Int Int
we hadn't UI. But when he/she wrote
> type family T where T = T1 Int Int
we had.

I can imagine now that it means we try to reduce Undecidable TF here. But
from client point it looks rather strange.

About technical details I answered personnaly.

Thanks,
Dmitry

2015-11-11 19:03 GMT+03:00 Richard Eisenberg <eir at cis.upenn.edu>:

> On Nov 11, 2015, at 10:43 AM, Dmitry Olshansky <olshanskydr at gmail.com>
> wrote:
>
> There are some questions / notes:
>
> 1. Could ghc use reduced "vanila types" for calculation with definition
> stored somewhere specially for error messages?
>
>
> Perhaps. But I'm not yet convinced that the current treatment of type
> synonyms is causing your slowdown.
>
>
> 2.  I didn't expect that type families can be without any parameters. But
> they really can. So instead of
> > type T2 = T1 Int Int
> I can write
> > type family T2 where T2 = T1 Int Int
> which is rather strange though.
> Moreover in this case ghc asks me for TypeFamilies and
> UndecidableInstances.
> In my scenario such code should write library-user. So including these
> (especially UndecidableInstances) extensions in his/her code is
> Undesirable.
>
>
> If your clients will have to include fancy type-level definitions, they
> will probably need UndecidableInstances. We're open to improving the
> termination checker if you have a good approach to how. :)
>
>
> 3. For type families more natural to have parameters but in this case we
> often can't reduce it deeply I suppose.
> Short simple example:
> type family L a b where
>   L a () = (a,())
>   L a (b,c) = (a,(b,c))
> type T1 = L Int ()
> type T2 = L Int T1
> type T3 = L Int T2
> type T3_Char = L Char T2
> and so on...
>
>
> I'm not sure what you're getting at here. Type synonyms and type families
> should behave the same (other than in error messages). Do you have an
> example where the compile time with type synonyms is demonstrably slower
> than the time with type families?
>
>
>
> Well, about my "complicated type-level program" now.  I start to play/work
> with well-known "named-fields" problem. My code is here
> <https://github.com/odr/pers>.
>
>
> Thanks for sharing your code. But it's very hard to understand what to
> look at here. I see in your "user application" link below that you have
> times. Are these compile times? Under what tests? Which version of GHC? We
> need to be really concrete so that I (or some other GHC dev) can reproduce
> what you're experiencing.
>
> Thanks!
> Richard
>
> I hoped to find decision with properties:
> - O(log n) time to get field from record by name
> - record construction independent from order of fields definitions
> - no TH preferrable, some TH possible
> - projections and joins are desirable
>
> I tried to implement it using "very-well balanced tree" (I don't know the
> right name) on type level.
> This is a binary search (by name) tree with count of left items is the
> same or one more than on the right side (for each subtree).
> The problem is construction. I realized it with FunDeps
> <https://github.com/odr/pers/blob/master/src/NamedBTree.hs> and  with TF
> <https://github.com/odr/pers/blob/master/src/NamedBTree2.hs>. User should
> write
> > type Rec = () <+ "a":>Int <+ "b":>Char <+ "c":>String
> > rec = () <+ (V "c" :: "c":>String) <+ (V 1 :: "a":>Int) <+ (V 'b' ::
> "b":>Char)
> or
> > rec = () <+ (V "c" :: "c":>String) <+ (V 1 :: "a":>Int) <+ (V 'b' ::
> "b":>Char) :: Rec
> and got
> rec = (((),V 1,()),V'b',((),V "c")) ::
> (((),"a":>Int,()),"b":>Char,((),"c":>String,())
>
> (Constructions like (V 1 :: "a" :> Int) rather ugly. Any ideas are
> welcomed... Perhaps some TH?)
>
> But compile time for user application
> <https://github.com/odr/pers/blob/master/app/Main.hs> is absolutely
> blocked this idea!
>
> I tried also to make a type-level sorted list
> <https://github.com/odr/pers/blob/master/src/List.hs> but it is also too
> complicated for ghc.
>
> I didn't check time with no-parameters-TF as you suggested. I will.
>
> Best regards,
> Dmitry
>
>
>
>
>
>
> 2015-11-11 16:43 GMT+03:00 Richard Eisenberg <eir at cis.upenn.edu>:
>
>> Users often introduce so-called "vanilla" type synonyms (with `type` but
>> not `type instance`) to be helpful abbreviations in code. As such, GHC
>> actually takes quite a bit of effort *not* to expand these, so that error
>> messages can report the synonyms instead of their expansions. On the other
>> hand, type /families/ tend to be used for type-level computation. So GHC
>> has decided to try to reduce all type families, while preserving all type
>> synonyms. This is all a bit arbitrary, and it should have no end-user
>> consequence except for error messages and, perhaps, performance.
>>
>> If you have a complicated type-level program whose compile time is
>> increasing faster than the program size, we'd love to know about it. We
>> (GHC devs) want type-level computation to be efficient!
>>
>> Thanks,
>> Richard
>>
>> On Nov 10, 2015, at 3:59 PM, Dmitry Olshansky <olshanskydr at gmail.com>
>> wrote:
>>
>> > Hello!
>> >
>> > It seems that types without parameters are not reduced in ghc unlike
>> CAFs.
>> >
>> > I.e. if we have
>> >
>> > type T1 a b = ...
>> > type T2 = T1 Int Int
>> >
>> > than T2 will be calculated on each utilization.
>> >
>> > Is my statement correct? If so, why is it?
>> > With complicated type-calculation compile time is growing too fast.
>> >
>> > Best regards,
>> > Dmitry
>> >
>> >
>> >
>> > _______________________________________________
>> > Haskell-Cafe mailing list
>> > Haskell-Cafe at haskell.org
>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151111/f31b4952/attachment.html>