Skip to content

[#608] Refactor Singletons for Peano and T

Danya Rogozinrequested to merge
danya/ghc-123-refactor-singletons into master

Problem: previously, the data type SingNat was storing SingNat n, KnownPeano n, and SingI n at the same time. This was consuming too much space at runtime. SingT was storing Sing t and SingI t at the time as well.

Solution: To get rid of those constraints, we introduce the data type PeanoNatural. The constructor PN stores SingNat n and Natural with the invariant that connect a natural number with the corresponding singleton. We define pattern synonyms Zero and Succ with the pragma {-# COMPLETE Zero, Succ #-} in order to preserve this invariant in pattern matching. We also get rid of the SingI constraint in constructors of SingT. We process values of this data type using the function withSingI from Data.Singletons.

This MR fixes #608 (closed).

Edited by Danya Rogozin

Merge request reports