erisco 2017-02-01 15:49:40
ghc also doesn't like inferring Sing types
erisco 2017-02-01 15:50:02
this explodes :t \x -> case x of STrue -> 1; SFalse -> 0
erisco 2017-02-01 15:51:04
seems a bit strange because what else could x be other than Sing (a :: Bool)
erisco 2017-02-01 15:51:16
you can just read it off the instance definition
ski 2017-02-01 15:54:26
EvanR : .. perhaps you're after the distinction between absolute and relative. affine space vs. vector space e.g.
nshepperd 2017-02-01 15:54:32
erisco: ghc doesn't try to do type inference on GADT pattern matching, iirc
nshepperd 2017-02-01 15:54:43
I don't know why but I assume there's a good reason
ski 2017-02-01 15:54:52
erisco : GADTs can't be inferred, nor families
erisco 2017-02-01 15:54:58
any idea how I import STrue and SFalse?
erisco 2017-02-01 16:02:05
supposedly it should just be Sing(STrue, SFalse)
erisco 2017-02-01 16:02:13
but I guess I need to get the right module, whoops
erisco 2017-02-01 16:02:50
nshepperd, where did you find that instance? what is the module?
erisco 2017-02-01 16:03:26
Data.Singletons.Prelude.Bool I am thinking
nshepperd 2017-02-01 16:03:57
erisco: yeah you can import the instance from that module
nshepperd 2017-02-01 16:05:11
the instance I found is from the github source at https://github.com/goldfirere/singletons/blob/023513fe2ee63391095540f575873064bbe3ab03/tests/ByHand2.hs
erisco 2017-02-01 16:05:11
okay, enabling the ever-confusing TypeInType…
nshepperd 2017-02-01 16:05:29
the actual Data.Singletons.Prelude.Bool module generates the instance with some template haskell
erisco 2017-02-01 16:05:39
%:== wrapped to give a more palatable Bool http://lpaste.net/351958
erisco 2017-02-01 16:06:19
now we're cooking with gas
erisco 2017-02-01 16:08:35
it is wild to me that we can have such an instance… they are singletons and yet here we are pattern matching
erisco 2017-02-01 16:09:28
is it just me? :P
erisco 2017-02-01 16:09:47
it is case analysis over multiple types
erisco 2017-02-01 16:10:09
not just multiple constructors but multiple types
erisco 2017-02-01 16:11:29
though I guess it cannot be any different than with a GADT
erisco 2017-02-01 16:11:48
you can do the same there I suppose
nshepperd 2017-02-01 16:13:24
it sort of is a GADT i guess
nshepperd 2017-02-01 16:13:57
like, there one instance for all types (b :: Bool) and it happens to be a GADT :O
erisco 2017-02-01 16:14:48
you could imagine just the GADT data X (b :: Bool) where STrue :: X 'True; SFalse :: X 'False
erisco 2017-02-01 16:15:02
and so pattern matching is just the same idea
erisco 2017-02-01 16:15:15
but I hadn't really thought of it like that
erisco 2017-02-01 16:17:50
ha, interesting, I think I actually want the TestEquality version of things because that proof is relevant
erisco 2017-02-01 16:18:48
just doing a little bounds checking and look at the can of worms I open…
erisco 2017-02-01 16:22:03
hehe, compiled!
erisco 2017-02-01 16:22:27
having to pattern match makes the code a bit… awful… but at least it works
erisco 2017-02-01 16:22:34
guards help a ton
erisco 2017-02-01 16:23:47
so I have sized vectors, right, but then I want to stuff some differently sized vectors in a container
erisco 2017-02-01 16:24:12
so I defined AnyVector as a GADT which stores the SNat for the size
erisco 2017-02-01 16:24:39
then I can pattern match and discover the size again… for example I can compare two AnyVector for equality
erisco 2017-02-01 16:24:41
sick or what
erisco 2017-02-01 16:25:19
I did it with almost no help too
erisco 2017-02-01 16:28:12
now what about type ordering
erisco 2017-02-01 16:28:26
Data.Type.Ordering where are you
erisco 2017-02-01 16:31:40
maybe I'll have to invent this one using Data.Type.Equality as reference
erisco 2017-02-01 16:32:50
glguy, do you know of a module?
mniip 2017-02-01 16:38:37
ski: poke
ski 2017-02-01 16:42:51
mniip : peek
mniip 2017-02-01 16:43:46
ski, an indefinite amount of time ago, you mentioned an internal language of a category, and I asked you what that meant and you didn't answer!
ski 2017-02-01 16:44:31
hm, internal language of which category ?
ski 2017-02-01 16:44:48
or just any topos ?
