#3005 closed feature request (fixed)
Normalize fully-applied type functions prior to display
Reported by: | dmcclean | Owned by: | chak |
---|---|---|---|
Priority: | lowest | Milestone: | 7.6.2 |
Component: | GHCi | Version: | 6.10.1 |
Keywords: | Cc: | jpm@…, pumpkingod@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
I have a module with a matrix type constructor:
> data (Natural r, Natural c) => Matrix r c t = Matrix [[t]] deriving (Eq)
which uses type-level naturals to provide dimension checking.
A type class for multiplication:
> class Multiply a b where > type Product a b > times :: a -> b -> Product a b
and an instance for matrix multiplication:
> instance (Natural a, Natural b, Natural c, Num t) => Multiply (Matrix a b t) (Matrix b c t) where > type Product (Matrix a b t) (Matrix b c t) = Matrix a c t > times m1 m2 = ...
All of this works really well, I get dimension checking (and inference), and lot of other goodies.
My request has to do with the following GHCi session:
*Main> let a = matrix two two [[1,1],[2,6]] *Main> :t a a :: Matrix Two Two Integer *Main> :t a `times` a a `times` a :: Product (Matrix Two Two Integer) (Matrix Two Two Integer)
When a type function is fully-applied, as Product is in this case, it would be nice if GHC could simplify it prior to display.
This would result in the following output for this example:
:t a `times` a a `times` a :: Matrix Two Two Integer
I have attached the files necessary to run this test case, although a simpler one could be constructed.
Attachments (4)
Change History (18)
Changed 10 years ago by
Attachment: | TypeNats.hs added |
---|
comment:1 Changed 10 years ago by
Owner: | set to chak |
---|
The problem is that sometime you want types to be normalised (like here), and sometimes, you prefer them non-normalised (e.g, when the normalised types get large). Currently, GHC tries to hard to print types with as little normalisation as possible (e.g, it prints String
instead of [Char]
).
So far, my plan was to leave that as it is, but provide a new ghci command to normalise a given type. This is useful for type-level programs (like in your code) without affecting the standard output. An extra ghci command has the advantage that you can "evaluate" type functions without needing to construct values that have the type that you want to evaluate (for :t
you always need to supply an appropriate expression).
Given your experience, would a new ghci command as described be sufficient for your purposes (without altering the behaviour of :t
)?
comment:3 Changed 10 years ago by
Description: | modified (diff) |
---|---|
difficulty: | → Unknown |
comment:4 Changed 10 years ago by
Milestone: | → 6.12 branch |
---|
comment:5 Changed 8 years ago by
Milestone: | 6.12 branch → 6.12.3 |
---|
comment:6 Changed 8 years ago by
Milestone: | 6.12.3 → 6.14.1 |
---|---|
Priority: | normal → low |
comment:7 Changed 8 years ago by
Cc: | pumpkingod@… added |
---|---|
Type of failure: | → None/Unknown |
comment:8 Changed 8 years ago by
Milestone: | 7.0.1 → 7.0.2 |
---|
comment:9 Changed 8 years ago by
Milestone: | 7.0.2 → 7.2.1 |
---|
comment:10 Changed 7 years ago by
Milestone: | 7.2.1 → 7.4.1 |
---|
comment:11 Changed 7 years ago by
Milestone: | 7.4.1 → 7.6.1 |
---|---|
Priority: | low → lowest |
comment:12 Changed 6 years ago by
Milestone: | 7.6.1 → 7.6.2 |
---|
comment:13 Changed 6 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
I believe this is fixed by the :kind!
command.
Changed 6 years ago by
Attachment: | Vectors2.hs added |
---|
Changed 6 years ago by
Attachment: | TypeNats2.hs added |
---|
comment:14 Changed 6 years ago by
For future reference, I paste the results of :kind! command and :type command.
Here is the result of :kind! command.
*Main> :kind! Product (Matrix Two Two Int) (Matrix Two Two Int) Product (Matrix Two Two Int) (Matrix Two Two Int) :: * = Matrix (O (I Z)) (O (I Z)) Int
And here are the results of :type command.
7.4.2
*Main> :t a `times` a a `times` a :: Matrix (O (I Z)) (O (I Z)) Integer
7.6.1
*Main> :t a `times` a a `times` a :: Matrix (O (I Z)) (O (I Z)) Integer
7.6.2 (7.6.1.20121207)
*Main> :t a `times` a a `times` a :: Matrix (O (I Z)) (O (I Z)) Integer
7.7.20130110
*Main> :t a `times` a a `times` a :: (Num t, Num t1, Multiply (Matrix Two Two t) (Matrix Two Two t1)) => Product (Matrix Two Two t) (Matrix Two Two t1)
(TypeNats.hs and Vectors.hs use -fglasgow-exts option. Vector uses DatatypeContexts. So, I attached newer version (TypeNats2.hs and Vector2.hs) what avoid using -fglasgow-exts option and DatatypeContexts.)
Type level naturals