Re: [Haskell-cafe] types calculation

...

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 :

On Nov 11, 2015, at 10:43 AM, Dmitry Olshansky 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 :

...

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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe