Open erikd opened 5 years ago
Yes, I have deprecated it for a while now, although I have started to maybe see it as a valid low-dependency/low compiletime replacement for singletons, so I might un-deprecate it in the future.
w.r.t singletons, the hackage documentation provides a migration guide: https://hackage.haskell.org/package/typelits-witnesses-0.3.0.3/docs/GHC-TypeLits-Witnesses.html#g:1
All of the functionality in this module can be subsumed by the singletons package, by utilizing:
- Data.Singletons
- Data.Singletons.TypeLits
- Data.Singletons.Prelude.Num
This module is left in this package as an alternative for those who might, for some reason, not want to add a singletons dependency to their project. However, if you do much at the type level, using the singletons library is much preferred, as it provides a unifed interface for all of the functionality here, generalized to other kinds besides
Nat
.For all functions in this module, a /singletons/ equivalent is included for help migrating.
In general:
The singletons type
Sing n
(or its equivalent,SNat n
) subsumes bothProxy n
andDict (KnownNat n)
. You can replace bothProxy n
andDict (KnownNat n)
withSNat n
to move to singletons style.
dictNatVal
andnatVal
are both justfromSing
.Replace
%+
,%-
, and%*
with their singletons equivalents,%+
,%-
, and%*
from Data.Singletons.Prelude.Num.%^
is in Data.Singletons.TypeLits.Use
withKnownNat
from /singletons/ (or just pattern match onSNat
) to get aKnownNat
instance from aSNat n
, the same way you'd get one from aDict
.The high-level combinator
withNatOp
can simply be replaced with applying your singleton functions (%+
etc.) toSNat
values, and pattern matching on the result, or usingwithKnownNat
on the result.
Ok, thanks! Will have to get my head around this.
Let me know if you would like any help migrating any specific piece of code :)
Managed to get most of this code ported over to use singletons, but I am stuck on this:
instance (KnownNat i, KnownNat o, KnownNat (i + o), i <= (i + o), o ~ ((i + o) - i)) => ... where
which worked fine with typelist-witnesses
, but with Data.Singleton.Prelude.Ord
that results in a type error:
• Expected a constraint, but ‘i <= (i + o)’ has kind ‘Bool’
I tried changing that line to:
instance (KnownNat i, KnownNat o, KnownNat (i + o), (i <= (i + o)) ~ 'True, o ~ ((i + o) - i)) => ... where
but that only causes this error:
• Could not deduce: (i <=? (i GHC.TypeNats.+ o)) ~ 'True
later in the code.
The problem seems to be that <=
was defined in your package as a Constraint
where as in singletons
its a Bool
.
Any clues to a solution to this much appreciated.
Ah yeah, the problem is that you need to bring in a witness of the inequality where you use a function that requires that inequality.
Typically you can get around this without any singletons using typechecker plugins like https://hackage.haskell.org/package/ghc-typelits-knownnat and http://hackage.haskell.org/package/ghc-typelits-natnormalise . However, if those fail, you need to find some other way of bringing in the constraint.
In this case, you can use the functions in GHC.TypeLits.Compare; in particular, isLE
or isNLE
, to compare two KnownNat
instances. This will give you Just Refl
as a result: if you pattern match on the Refl
, then GHC will be happy with the (i <=? (i GHC.TypeNats.+ o)) ~ 'True
constraint within the body of the pattern match.
n.b. I have uploaded a new release that overhauls GHC.TypeLits.Witnesses to be more or less a lite singletons clone as it pertains only to Nat
and Symbol
.
I would like to avoid the extra complication of compiler plugins, but I don't really understand the option involving GHC.TypeLits.Compare
(version 0.4.0). I can use isLE
like this:
instance (KnownNat i, KnownNat o, KnownNat (i + o), isLE i (i + o), o ~ ((i + o) - i)) => ... where
but that doesn't work. It doesn't seem to be a complete solution and I don't understand the rest of your proposed solution.
If its of any help, the code is in the last two commits here: https://github.com/HuwCampbell/grenade/tree/topic/singletons
Sorry for not getting back earlier; I've been on vacation :)
isLE
is not a type-level function, but rather it's a normal value-level function. It's a way to get the i <= i + o
constraint "in scope", if you need it.
The main thing you would do at the value level is require something like i <= i + o
, and then when you need to use the instance, use isLE
to bring that constraint into scope in order to properly call it.
With ghc 8.6.5, I get a deprecation warning with this module that suggests:
but the
singletons
package does not seem to have a repalcement. What am I missing?