Opened 6 years ago

Closed 2 years ago

Last modified 2 years ago

#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)

TypeNats.hs (16.7 KB) - added by dmcclean 6 years ago.
Type level naturals
Vectors.hs (4.0 KB) - added by dmcclean 6 years ago.
Matrix math library
Vectors2.hs (4.0 KB) - added by shelarcy 2 years ago.
TypeNats2.hs (16.8 KB) - added by shelarcy 2 years ago.

Download all attachments as: .zip

Change History (18)

Changed 6 years ago by dmcclean

Type level naturals

Changed 6 years ago by dmcclean

Matrix math library

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:2 Changed 6 years ago by dreixel

  • Cc jpm@… added

I would be happy with a new ghci command.

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 4 years ago by pumpkin

  • Cc pumpkingod@… added
  • Type of failure set to None/Unknown

comment:8 Changed 4 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 2 years ago by monoidal

  • Resolution set to fixed
  • Status changed from new to closed

I believe this is fixed by the :kind! command.

Changed 2 years ago by shelarcy

Changed 2 years ago by shelarcy

comment:14 Changed 2 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.)

Note: See TracTickets for help on using tickets.