[Haskell-cafe] types calculation

[Dmitry Olshansky]

There are some questions / notes:

1. Could ghc use reduced "vanila types" for calculation with definition
stored somewhere specially for error messages?

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.

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


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>.
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/67bedddb/attachment.html>