A standard library for semi-fancy types?

Inspiration struck me tonight and I drafted my own inductive unary integers. I then used them to define quantities tagged by their dimensions, so that the formulae constructed out of them are sound from the point of view of dimensional analysis. The project uses experimental features of GHC here and there, but you should be able to compile this particular file with ghc -XUndecidableInstances -XTypeFamilies -XDataKinds -XUnicodeSyntax ℤ.hs if you would like to.

My numbers sort of work, but it feels like such a waste of effort. Surely there should be a standard library for this sort of thing? I know there are natural numbers in GHC.TypeLits, but they seem to not be suitable for this task since they are not inductive. And ideally, I suppose we should like to use binary arithmetic and not unary? Then, add some property checks by generating a large number of examples with Template Haskell and seeing if they compile… Not a small work! At the same time, it is not fancy enough to be of interest to the research community — the path is well trodden.

Is anyone else doing this sort of stuff? Does anyone care? What is the grand strategy for standard semi-fancy types in Haskell?

A cursory search revealed this:

  • type-level-integers. Small and nice, very easy to understand. Provides inductive type level integers that live in their own kind. If I wanted to explain type level programming to a stranger, I should use this one as an example.
  • numtype-tf. Despite the name, most of the functionality is written as class instances, not type families. I think this one is more or less obsolete.
  • numtype-dk. This one actually uses type families for everything. But it looks as though it simply enumerates a bunch of possible numbers, like literally «1 2 3».
  • tfp. Very fancy, source is not immediate to understand. So fancy that I am actually afraid to voice any value judgements.

None of these packages appear to be frequently used and in any sense «standard». There is so much wisdom in there — why this design choice was made and not the other — but it is not easily accessible.

On a final note — I should really like to have a special notation for type level numbers other than GHC.TypeLits.Nat. Maybe some sort of a magic two parameter type class can be constructed that witnesses the correspondence of a certain type to a certain Nat? It would work similarly to how functions toList and fromList are used to define overloaded lists, only at the type level. GHC then would use it to convert number literals to any custom kind of integers.

I do not really want to deliver one single message in this post. Rather, I want to start a conversation. Fancy types are a lonely place to be in.

2 Likes

I struggled with Nat in GHC.TypeLits too. But now I think you can go quite a distance with them.
What I would really like to see is standard GHC.TypeLits.Nat.Theory module with bunch of simple
propositions for Data.Type.Equality constructions. Things like n + m :~: m + n.

E.g. (I should not have needed to write these) https://github.com/rpeszek/present-proofs-lc19/blob/master/src/Present/WorkingWithTypeLits.hs

Compare this with Nat versions:
https://github.com/rpeszek/IdrisTddNotes/blob/master/src/Data/SingBased/NatTheorems.hs

You should be able to do induction with GHC.TypeLits Nat using 0 and n + 1 (that would map closely to Z and S). Sometimes using 0 and n - 1 seemed to work easier when I tried it:
https://github.com/rpeszek/IdrisTddNotes/wiki/Part2_Sec6_2_1_adder
I think using both approaches (n + 1 vs n - 1) should be largely equivalent, they just avoid the need for Refl trickery in different places.
In fact, the biggest advantage of using DataKinds with Peano like definition (Z and S constructors) is that GHC compiler can prove more properties automatically making it easier to write code. The program can supply such information to the compiler, this just requires some extra code. Thus, IMO, working with Peano inductive definition does not provide that much advantage.

I do agree that having Nat that exposes Z and S constructors would be nice. It would be great if there was some magic rewrite rules that translated
a slow inductive type with Z and S to a fast primitive type with binary layout like the GHC Nat. Does Idris do that now?

Being on the type level, the toList and fromList equivalents would be type families.

E.g.
https://github.com/rpeszek/IdrisTddNotes/blob/master/src/Data/SingBased/Nat.hs#L77

And probably will be harder to make them as nice and implementation agnostic.

I want to sum up my thoughts / questions:

  • I would really love to see base include (a zero runtime cost) theory module with propositions about Nat. When using type level Nat you get compilation issues very fast. Maybe singletons-base package could include such module instead?
  • Could a standard Peano like (value level) Nat with S and Z constructor be somehow converted to a primitive type like GHC.Types.Nat under the hood?
3 Likes