erisco 2017-02-01 13:48:18
are there integers or naturals bounded by type, yet?
monochrom 2017-02-01 13:55:53
No.
erisco 2017-02-01 13:56:38
but I might get away with smart constructors
erisco 2017-02-01 13:56:42
at least it is a half-measure
monochrom 2017-02-01 13:56:51
Yes, I would start with that.
erisco 2017-02-01 13:57:17
well I began with even looser and I am looking for ways to tighten it up
erisco 2017-02-01 14:19:11
is there any sensible way we can compare SNat a with SNat b?
_raynold_ 2017-02-01 14:20:29
ahh it's a wonderful day
erisco 2017-02-01 14:21:23
it can't be with == of course
ski 2017-02-01 14:28:40
erisco : `SNat' ?
erisco 2017-02-01 14:29:00
yeah should be something with %:==
Welkin 2017-02-01 14:29:08
why not make an Eq instance?
erisco 2017-02-01 14:29:24
it is impossible because they are different types
glguy 2017-02-01 14:29:55
erisco: How about http://hackage.haskell.org/package/base-4.9.1.0/docs/Data-Type-Equality.html#t:TestEquality
Welkin 2017-02-01 14:29:57
is it an instance of Num?
erisco 2017-02-01 14:30:03
no
ski 2017-02-01 14:31:03
erisco : dunno what `(%:==)' is, either ..
erisco 2017-02-01 14:31:15
https://hackage.haskell.org/package/singletons-2.2/docs/Data-Singletons-Prelude-Eq.html#v:-37-:-61--61-
erisco 2017-02-01 14:34:09
so then I end up with either Sing 'True or Sing 'False
erisco 2017-02-01 14:34:25
can I branch on this is the next question
ski 2017-02-01 14:34:26
erisco : looks similar to and
glguy 2017-02-01 14:34:42
erisco: Did you see my link?
erisco 2017-02-01 14:36:15
yes, maybe I need to look harder
glguy 2017-02-01 14:36:33
or you can respond explaining why it doesn't help too
glguy 2017-02-01 14:36:43
I haven't read all the way back, so it might not
ski 2017-02-01 14:36:54
oh, `Data.Type.Equality' is in `base'
ski 2017-02-01 14:38:10
.. i assume `inner' and `outer' there needn't work with type families (?)
erisco 2017-02-01 14:38:41
glguy, it seems to solve what I am looking for. I have to grasp these concepts better
erisco 2017-02-01 14:39:09
I am not sure, for example, why Maybe (a :~: b)
ski 2017-02-01 14:40:03
in case `a' and `b' are not equal types, or otherwise in case the two values of type `f a' and `f b' are not equal values, it gives `Nothing'
nshepperd 2017-02-01 14:40:04
erisco: you'll need to pattern match on the SNat, to bring out the KnownNat constraint, which has runtime info about what Nat it is
glguy 2017-02-01 14:40:28
so that when you learn that the arguments are true both at the value and type level
glguy 2017-02-01 14:40:32
are equal*
nshepperd 2017-02-01 14:40:40
if natVal (Proxy @ a) == natVal (Proxy @ b), then you can manufacture a proof that a ~ b
nshepperd 2017-02-01 14:41:35
or I suppose you can just return a Bool
erisco 2017-02-01 14:41:54
well that is what I am wondering… why not Bool
erisco 2017-02-01 14:42:05
the term is either Nothing or Just Refl
nshepperd 2017-02-01 14:42:19
but proof such as '(a :~: b)' is more useful
nshepperd 2017-02-01 14:42:56
because pattern matching it brings 'a ~ b' into scope, and the type checker can assume that they are equal from that point on
erisco 2017-02-01 14:43:31
ah, makes sense
erisco 2017-02-01 14:44:23
so I wonder how this contrasts with Data.Singletons.Prelude.Eq
ski 2017-02-01 14:44:47
forall k. forall (f :: k -> *) (a :: k) (b :: k). forall (fa :: f a) (gb :: g b). (testEquality fa gb = Nothing => a =/= b \/ fa =/= gb) /\ (testEquality fa gb = Just Refl => fa = gb)
ski 2017-02-01 14:44:57
would presumably be the law for `testEquality'
erisco 2017-02-01 14:44:59
with %:== we find either Sing 'True or Sing 'False
