#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 Revisions: |
Description (last modified by igloo)
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 6 years ago by dmcclean
comment:1 Changed 6 years ago by chak
- 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 6 years ago by igloo
- Description modified (diff)
- difficulty set to Unknown
comment:4 Changed 6 years ago by igloo
- Milestone set to 6.12 branch
comment:5 Changed 5 years ago by igloo
- Milestone changed from 6.12 branch to 6.12.3
comment:6 Changed 5 years ago by igloo
- Milestone changed from 6.12.3 to 6.14.1
- Priority changed from normal to low
comment:7 Changed 5 years ago by pumpkin
- Cc pumpkingod@… added
- Type of failure set to None/Unknown
comment:8 Changed 5 years ago by igloo
- Milestone changed from 7.0.1 to 7.0.2
comment:9 Changed 4 years ago by igloo
- Milestone changed from 7.0.2 to 7.2.1
comment:10 Changed 4 years ago by igloo
- Milestone changed from 7.2.1 to 7.4.1
comment:11 Changed 3 years ago by igloo
- Milestone changed from 7.4.1 to 7.6.1
- Priority changed from low to lowest
comment:12 Changed 3 years ago by igloo
- Milestone changed from 7.6.1 to 7.6.2
comment:13 Changed 3 years ago by monoidal
- Resolution set to fixed
- Status changed from new to closed
I believe this is fixed by the :kind! command.
Changed 3 years ago by shelarcy
Changed 3 years ago by shelarcy
comment:14 Changed 3 years ago by shelarcy
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