A standard library for semi-fancy types?

Learn
#1

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.

4 Likes
Iterated currying and mapping — better solutions?
#2

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?
5 Likes
#3

Also check out Galois’s parameterized-utils, a library that provides a kind of “prelude” for parameterized types with arbitrarily kinded parameter types. Data.Parameterized.NatRepr might be of interest – it provides a runtime representation of Nat which can be pattern matched on to recover the Nat at runtime, as well as a number of proof combinators for convincing GHC’s unforgiving (in this regard) typechecker that various equalities/inequalities hold. We developed it after a lot of using fancy types in practice. Paper here.

4 Likes
#4

See also this question. An answer suggests that the induction principle can be postulated on any type, and specifically on Nat, with unsafeCoerce Refl or something like that. I am not sure how to wield it yet.

#5

I’d love to hear more about what you’re using doing with dimensional analysis. A library that let me do engineering calculations which were (dimensionally) well-typed would be very nice

#6

I was trying to attach dimensions to some basic economic computations like interest over time. It worked to some extent, but nothing much came out of it.

I know there have been several attempts to describe dimensions of physical values at the type level. There are some libraries on Hackage. But I never tried any of them because they appear not to be suitable for representing interest over time.

I am sure you will find a better learned person to talk about it to if you ask around.

1 Like
#7

I would like to revive this thread. I totally agree. Shouldn’t there be a “standard” inductive Nat type package, together with proofs such as those we can find in Lean and Mathlib ? I suppose for the moment the logical thing would be for that package to use the singletons package ? I’m creating some proofs on my own, but I would like to contribute them somewhere. There would need to be agreement on how to encode <= and < and some other things. Also “there exists x such that” would be done via Data.Singletons.Sigma ? I haven’t really been able to understand yet how we can create “type lambdas” to be able to use Sigma for stuff such as “there exists l such that m + l :~: n” which would correspond to a lambda (\l → m + l :~: n). Is this possible already in an ergonomic way, or requires creating other auxiliary data types ?

#8

Also, is there a document I can refer to understand the design decision behind Nat in GHC.TypeLits ? It just seems to be unusable (or quite hard) to do proofs… I would like to understand why this was chosen instead of the usual inductive definition with Zero and Succ. Thanks !

1 Like