ski 2017-02-01 14:45:31
@where boolean-blindness
lambdabot 2017-02-01 14:45:32
http://existentialtype.wordpress.com/2011/03/15/boolean-blindness/
ski 2017-02-01 14:45:37
erisco ^
erisco 2017-02-01 14:45:59
I've read about boolean blindness so much that I am nearly blind from it
erisco 2017-02-01 14:46:52
just off hand I know what True or False implies. and yes, the type system doesn't
erisco 2017-02-01 14:47:20
which is a strangeness I may never get over
ski 2017-02-01 14:47:59
erisco : afaics, that `Data.Singletons.Prelude.Eq' gives a type-level `Bool'
nshepperd 2017-02-01 14:48:13
hmm, well I suppose you can pattern match on your result of %:== to get either (STrue :: Sing True) or (SFalse :: Sing False)
nshepperd 2017-02-01 14:48:59
then knowing that (a :== b) ~ 'True tells you that a ~ b
erisco 2017-02-01 14:49:02
how do you pattern match? Sing is a data family
glguy 2017-02-01 14:51:33
With Maybe (a :~: b) you get 4 results: undefined, no idea; Nothing, probably not equal; Just undefined, probably equal; Just Refl, definitely equal :)
nshepperd 2017-02-01 14:52:35
Sing is only open in the kind argument, afaict
nshepperd 2017-02-01 14:53:04
data Sing Bool where { SFalse :: Sing Bool False; STrue :: Sing Bool True }
erisco 2017-02-01 14:53:48
but STrue has type Sing 'True, not Sing Bool
nshepperd 2017-02-01 14:54:11
Sing secretly has two arguments
erisco 2017-02-01 14:54:21
the point of the whole thing, I thought, was they were singletons
nshepperd 2017-02-01 14:54:23
data family Sing k (a :: k)
ski 2017-02-01 14:54:28
`Sing :: (k :: Kind) -> k -> *', iiuc
ski 2017-02-01 14:54:51
(or perhaps it should be written as `Sing :: forall k. k -> *' ?)
erisco 2017-02-01 14:55:29
oh janky, so it can take a kind parameter in what is otherwise a type position?
nshepperd 2017-02-01 14:55:33
it's a bit annoying and confusing that the kind argument isn't written out explicitly
ski 2017-02-01 14:55:41
hmm .. this whole `~>' business here looks interesting
hpc 2017-02-01 14:56:02
is this that whole kind in kind thing?
nshepperd 2017-02-01 14:56:34
erisco: so Sing is a type family that takes a kind, and maps to a data declaration with a singleton for each inhabitant of that kind
nshepperd 2017-02-01 14:56:49
SFalse :: Sing Bool False
nshepperd 2017-02-01 14:56:59
STrue :: Sing Bool True
nshepperd 2017-02-01 14:57:37
SNat :: (KnownNat n) => Sing Nat n
erisco 2017-02-01 14:57:38
that just doesn't fly in my ghci
nshepperd 2017-02-01 14:57:47
approximately
ski 2017-02-01 14:57:55
hpc : dunno
nshepperd 2017-02-01 14:58:04
ghc doesn't like you to write out the kind argument explicitly
erisco 2017-02-01 14:58:28
is that so
erisco 2017-02-01 14:58:49
you're revealing some elite secrets right here nshepperd
nshepperd 2017-02-01 14:59:36
let f :: Sing (a :: Bool) -> String; f STrue = "yay"; f SFalse = "boo" -- this is totally allowed though
ski 2017-02-01 15:00:02
erisco : "it can take a kind parameter in what is otherwise a type position" -- rather, i think it can either explicitly take the implicit kind argument .. either that, or it's just sloppy in printing out an application of `Sing' with the kind argument like an explicit argument (rather than writing something like `Sing @Bool False', say)
erisco 2017-02-01 15:00:40
why does this just say data family Sing (a :: k) https://hackage.haskell.org/package/singletons-2.2/docs/Data-Singletons.html#t:Sing
ski 2017-02-01 15:01:18
it would perhaps be nicer if it said `data family forall k. Sing (a :: k)' ..
ski 2017-02-01 15:01:37
the point is that `Sing' is a polymorphic type (family)
ertes 2017-02-01 15:02:11
-XTypeInType should allow this, i think: Sing k (a :: k)
ski 2017-02-01 15:02:29
presumably
ski 2017-02-01 15:02:50
(.. what else would it be good for ?)
Jello_Raptor 2017-02-01 15:03:11
so, a transitive Newtype class is a bad idea, right? (i.e `instance (Newtype a b,Newtype b c) => Newtype a c where ...`) It needs Undecidable-Instances and means the typechecker won't halt until it hits the recursion limit?
erisco 2017-02-01 15:03:59
okay, while I am still confused on this Sing kind thing, I am also confused on SFalse and STrue
ertes 2017-02-01 15:04:01
a lot of the fancy features of -XTypeInType (like kind classes and kind families) boil down to this consistency
erisco 2017-02-01 15:04:11
if I ask :t STrue :: Sing 'True it is happy
erisco 2017-02-01 15:04:19
if I ask :t STrue :: Sing Bool it is not happy
erisco 2017-02-01 15:04:30
yet the definition of Sing Bool has STrue as a constructor
erisco 2017-02-01 15:04:53
but it seems haddock is mucked up and not printing it right
erisco 2017-02-01 15:05:06
if you expand the Sing Bool definition
erisco 2017-02-01 15:05:26
wrong source location too
erisco 2017-02-01 15:05:51
so what is this SingBool z? why is STrue :: Sing 'True but not STrue :: Sing Bool according to ghci?
nshepperd 2017-02-01 15:06:07
it's not "STrue :: Sing Bool"
nshepperd 2017-02-01 15:06:24
STrue :: Sing Bool 'True -- conceptually, with the kind parameter explicitly written as an argument. ghci won't accept this
ski 2017-02-01 15:06:24
if you wanted it explicit, it'd be : STrue :: Sing Bool 'True
ski 2017-02-01 15:06:31
not just `STrue :: Sing Bool'
nshepperd 2017-02-01 15:06:50
STrue :: Sing (True :: Bool) -- the actual syntax
erisco 2017-02-01 15:07:44
okay I think I see what is happening
erisco 2017-02-01 15:08:22
why would they choose Sing (a :: k) to mean k as a kind parameter, and "a" not as a parameter at all
erisco 2017-02-01 15:08:35
because the obvious reading is that "a" is a type parameter of any kind
erisco 2017-02-01 15:09:00
how would you even write such a parameter then? a type of any kind?
nshepperd 2017-02-01 15:09:03
tbh my brain is about to explode here
erisco 2017-02-01 15:09:59
in 30 years they'll be laughing at this as the Perl of type systems I'm sure
erisco 2017-02-01 15:10:09
but we have to deal with the state of the art for now ;)
EvanR 2017-02-01 15:10:29
lets say you have an "result of ADC" type which conceptually goes from 0 to 1023. now levels dont have sensible arithmetic like numbers, since if you added 1 to 1023 it would go off the scale
ski 2017-02-01 15:10:36
`Sing (a :: k)' is really just a verbose form of `Sing a'. the `:: k' there is just a kind ascription. it just so happens that the kind of this argument is equal to the kind that *is* the implicit argument, so by explicitly using a kind ascription, you're simultaneously constraining the implicit kind argument to be that kind
EvanR 2017-02-01 15:10:52
besides converting to a number, what are some sensible operations that DO make sense for these levels?
EvanR 2017-02-01 15:11:28
min, max
erisco 2017-02-01 15:11:36
"Sing (a :: k)" is verbose for "Sing a" yes I thought this
EvanR 2017-02-01 15:11:40
normalized multiplication
nshepperd 2017-02-01 15:11:42
EvanR: saturating arithmetic?
erisco 2017-02-01 15:11:46
what I do not understand is where this implicit argument comes from
ski 2017-02-01 15:11:55
this is similar to calling `typeOf (Proxy :: Proxy Bool)', where `typeOf :: forall a. Typeable a => proxy a -> TypeRep'. by using the type ascription `:: Proxy Bool', we're constraining the implicit type argument `a' to be equal to `Bool'
nshepperd 2017-02-01 15:11:55
I think the situation is sort of similar to a value level polymorphic function?
EvanR 2017-02-01 15:12:08
ah saturating addition, saturating scaling by a scalar
erisco 2017-02-01 15:13:30
I just don't follow
nshepperd 2017-02-01 15:13:31
'foo :: forall a. a -> String' has a sort of implicit argument which is the type parameter
erisco 2017-02-01 15:13:52
how is it any sense that Sing x y is Sing (y :: x)
nshepperd 2017-02-01 15:15:20
something something system F
erisco 2017-02-01 15:15:37
it is so supremely confusing
erisco 2017-02-01 15:15:53
how would you write a parameter which had a polymorphic kind?
EvanR 2017-02-01 15:15:55
clearly x has to be a type here, and y might be a type
erisco 2017-02-01 15:15:55
it is impossible then
erisco 2017-02-01 15:17:03
because if F Y means F (x :: Y) then it cannot also mean F Y
muyfine 2017-02-01 15:17:08
I'm having trouble with doing things inside of a conduit: http://lpaste.net/4319257805665075200
erisco 2017-02-01 15:17:16
unless we're overloading the syntax based on whether Y is recognised as a kind or type
ski 2017-02-01 15:17:18
EvanR : cut-off / truncating subtraction, aka monus
nshepperd 2017-02-01 15:17:19
I think maybe haddock is printing the data instances in some confusing wrong way
muyfine 2017-02-01 15:17:21
I have to explicitly use a "lift"
erisco 2017-02-01 15:17:42
I mean it cannot mean F (Y :: k)
muyfine 2017-02-01 15:17:45
but only inside the conduit - things are fine everywhere else
nshepperd 2017-02-01 15:17:56
erisco: for instance I can write 'data family Bar (a :: k); data instance Bar Int = BI; data instance Bar 4 = B4' and that does pretty much what you expect
muyfine 2017-02-01 15:18:13
I'm trying to figure out how I can remove the lift usage
nshepperd 2017-02-01 15:18:15
BI :: Bar Int
nshepperd 2017-02-01 15:18:20
B4 :: Bar 4
EvanR 2017-02-01 15:18:20
ski: are you sure that makes sense, or are we thinking of truncating / cut-off subtraction of a real number from a level
nshepperd 2017-02-01 15:18:43
in ghci
EvanR 2017-02-01 15:18:55
like the difference between adding subtracting number of days from a date, but not adding subtracting dates
ski 2017-02-01 15:19:00
EvanR : "how is it any sense that Sing x y is Sing (y :: x)" -- it isn't. it's the case that `Sing x (y :: x)' would be the same as `Sing x y', assuming we had `Sing :: (x :: Kind) -> x -> *' (which we don't)
ski 2017-02-01 15:19:04
er
EvanR 2017-02-01 15:19:05
er, adding dates rather
ski 2017-02-01 15:19:06
erisco ^
erisco 2017-02-01 15:19:13
nshepperd, I don't know what to expect anymore
erisco 2017-02-01 15:19:31
nshepperd, is Int interpreted as a kind? a type? what about 4?
nshepperd 2017-02-01 15:20:12
erisco: these are both types
nshepperd 2017-02-01 15:20:19
Int is a type of kind *
mniip 2017-02-01 15:20:22
hey ski
nshepperd 2017-02-01 15:20:24
4 is a type of kind Nat
ski 2017-02-01 15:20:28
erisco : however, now the kind argument is not explicit like in `Sing :: (x :: Kind) -> x -> *', but implicit like in `Sing :: forall x. x -> *', so our two equivalent type expressions then becomes `Sing (y :: x)' resp. `Sing y' -- as you can see, in the former case, we're still (indirectly) explicitly fixing the type to `x', while in the second case, we're not
ski 2017-02-01 15:20:44
EvanR : why wouldn't it make sense ?
nshepperd 2017-02-01 15:20:48
erisco: this is the 'argument of any kind' you wanted
erisco 2017-02-01 15:20:49
nshepperd, but this doesn't seem to touch the case with Sing
erisco 2017-02-01 15:21:01
because with Sing we're writing Sing K where K is a kind
nshepperd 2017-02-01 15:21:10
erisco: I just found the actual syntax for doing what Sing is doing. haddock is wrong
nshepperd 2017-02-01 15:21:32
erisco: it looks like 'data instance Sing (b :: Bool) where { SFalse :: Sing 'False; STrue :: Sing 'True }'
erisco 2017-02-01 15:21:32
what you described nshepperd is exactly how I'd expect it to work, but Sing deviates from this
ski 2017-02-01 15:21:42
EvanR : it is defined by ⌜m ∸ o ≤ n ⇔ m ≤ n + o⌝
EvanR 2017-02-01 15:22:08
ski: i asked why it would make sense, a possible answer is you can think of levels by their imagine into a number type, which can obviously do any arithmetic. but then you could also add dates, or whatever you want, anything makes sense if you work in the image of some conversion function
EvanR 2017-02-01 15:22:42
and in this case also having a canonical truncation to convert back with
ski 2017-02-01 15:23:00
EvanR : i have no idea what this `ADC' is meant to describe (my first association is "ADd with Carry")
EvanR 2017-02-01 15:23:02
if thats youre answer, then i want to ask what are some useful operations on levels
EvanR 2017-02-01 15:23:09
ski: analog to digital conversion
ski 2017-02-01 15:24:05
EvanR : .. hmm, what if you added values `NegInf' and `PosInf' ?
EvanR 2017-02-01 15:24:07
like 0 might not mean numeric zero, 0 and 1023 are just extreme "left" and "right" of some needle
ski 2017-02-01 15:24:19
(representing "off the scale")
erisco 2017-02-01 15:24:19
ski you mean Sing :: (x :: Kind) -> y -> * ?
EvanR 2017-02-01 15:24:46
subtraction kind of exposes which direction is "positive"
EvanR 2017-02-01 15:24:52
and so does addition
EvanR 2017-02-01 15:25:09
reflection doesnt, "one minus"
EvanR 2017-02-01 15:25:56
appending two off-the-scale values sounds useful
erisco 2017-02-01 15:25:59
nshepperd, that is interesting. I was not aware such a thing was possible
erisco 2017-02-01 15:26:12
and neither did haddock :P
erisco 2017-02-01 15:26:22
and instance for all types of a kind
EvanR 2017-02-01 15:27:20
ski: when messing with microcontrollers i noticed that the decisions of whether to assign 0 or 1023 to the high or low or left or right or whatever real world thing is hard to remember and ultimately arbitrary
erisco 2017-02-01 15:27:20
I understand from that nshepperd how it works
EvanR 2017-02-01 15:27:48
i blame the mentioning of numbers completely on the C language used to program them
erisco 2017-02-01 15:27:55
:k 'True :: Bool and :k 'False :: Bool
lambdabot 2017-02-01 15:27:57
error: parse error on input '::'
ski 2017-02-01 15:28:05
erisco : no, i meant what i said, `Sing :: (x :: Kind) -> x -> *' , meaning that `Sing' is a type (function) that takes two arguments, (a) a *kind* (which is named `x', so that we can refer to it later); and (b) a type (of kind `x'); returning a concrete type (iow a type of kind `*')
erisco 2017-02-01 15:28:32
*shrug* I don't understand it ski
EvanR 2017-02-01 15:29:07
maybe the natural operations im looking for here are things that shift levels one way or the other, like a mobius transformation
ski 2017-02-01 15:29:27
erisco : so, since `Bool' is a kind, then `Sing Bool :: Bool -> *'; and since 'True is a type of kind `Bool', also Sing Bool 'True :: *
erisco 2017-02-01 15:29:37
ski, oh, never mind, I understand your notation now
EvanR 2017-02-01 15:29:39
and levels themselves dont have any binary algebra
ski 2017-02-01 15:29:40
erisco : how much do you know about dependent types ?
erisco 2017-02-01 15:29:49
enough to get confused like this
ski 2017-02-01 15:30:42
erisco : perhaps a better notation would be `Sing :: (x ::) Kind -> x -> *', to say that the first argument of `Sing' should be a `Kind' (and btw, we're going to call it `x'), the second argument should be a type of kind `x', the result will be a type of kind `*'
ski 2017-02-01 15:33:01
EvanR : did you mean like a möbius band ?
EvanR 2017-02-01 15:33:07
i dont think so
erisco 2017-02-01 15:33:22
though now we know the printing of "Sing Bool" was wrong to begin with
ski 2017-02-01 15:33:26
erisco : "how would you write a parameter which had a polymorphic kind?" -- did you mean ".. which had a kind that was a kind variable" ?
erisco 2017-02-01 15:33:29
so there really isn't the confusion now
erisco 2017-02-01 15:33:51
there was no Sing Bool anytime anywhere
ski 2017-02-01 15:34:07
erisco : anyway, as i said, i wish GHC/Haddock would make up its mind about whether the argument in this case is implicit or explicit (by default)
EvanR 2017-02-01 15:34:21
they are automorphisms of the riemann sphere
erisco 2017-02-01 15:34:21
the instance was instance data Sing (a :: Bool)
erisco 2017-02-01 15:34:27
not Sing Bool
erisco 2017-02-01 15:34:35
and in usage it is Sing 'True or Sing 'False, not Sing Bool
erisco 2017-02-01 15:35:00
and STrue :: Sing 'True, SFalse :: Sing 'False, 'True :: Bool, 'False :: Bool
erisco 2017-02-01 15:35:05
all seems well
erisco 2017-02-01 15:35:43
an instance that I was not aware was even possible, but it checks out
erisco 2017-02-01 15:37:10
so then, quite simply, I can pattern match as you say nshepperd
ski 2017-02-01 15:37:16
(needing some auxiliary syntax to specify explicitly an otherwise implicit argument (cf. ), and to not specify explicitly an otherwise explicit argument (cf. ))
erisco 2017-02-01 15:37:17
using %:==
ski 2017-02-01 15:37:27
EvanR : ok
erisco 2017-02-01 15:37:46
then I suppose it is another discussion as to how this relates with :~:
EvanR 2017-02-01 15:38:12
literally doing analysis with real numbers isnt really helping much, since you have numeric value
EvanR 2017-02-01 15:38:33
theres some symmetry broken by choosing which side to encode as a zero
ski 2017-02-01 15:39:06
.. i'm not seeing how analysis and the Riemann sphere relates to these digital levels ?
EvanR 2017-02-01 15:39:31
and on all the operations you need to make sure the encoding remains consistent
EvanR 2017-02-01 15:39:53
as a user, it really should be irrelevant, an implementation detail
EvanR 2017-02-01 15:40:02
like the choice of day number zero in history
EvanR 2017-02-01 15:40:42
ski: well ignore that, instead maybe operations "shift toward left, shift toward right, by an integer, then clamp"
erisco 2017-02-01 15:41:21
I guess the simple picture is that SEq is really just applying Eq to singletons for the sake of it
erisco 2017-02-01 15:41:29
and :~: is about proofs of type equality
EvanR 2017-02-01 15:44:44
we "turn things up to 11" so much that we think of levels and numbers the same!
