erisco 2017-02-04 18:45:41
you're right, I could have just defined data NatEq (a :: Nat) (b :: Nat) where EqZ ... EqS ...
jle` 2017-02-04 18:45:50
data NatEq :: Nat -> Nat -> * where EqZ :: NatEq Z Z; EqS :: NatEq n n -> NatEq (S n) (S n)
jle` 2017-02-04 18:45:52
yeah
jle` 2017-02-04 18:47:00
using a data family lets you use the ':=' identifier for your eq witnesses for different types
erisco 2017-02-04 18:47:02
I suppose the difference is NatEq constructs a *
jle` 2017-02-04 18:47:17
well, so does :=
erisco 2017-02-04 18:47:24
yes I know
erisco 2017-02-04 18:47:34
I just mean that I don't need a := kind
erisco 2017-02-04 18:47:40
whereas I need a Nat kind
erisco 2017-02-04 18:48:13
so I guess it is moreso that Nat defines the types/kind and SNat defines the terms/type
erisco 2017-02-04 18:48:29
but still seems a bit strange for some reason
mniip 2017-02-04 18:48:34
• Expected kind 'N (NF 'Nothing)',
mniip 2017-02-04 18:48:35
but ''Z' has kind 'N (NF 'Nothing)'
mniip 2017-02-04 18:48:36
hahah
erisco 2017-02-04 18:48:59
careful mniip. you're causing netsplits with your exploits
jle` 2017-02-04 18:49:02
yeah. Nat gives you the kind and the types, and SNat is the witnesses of those that you can pass around at the value level
mniip 2017-02-04 18:49:12
that's not a netsplit...
erisco 2017-02-04 18:49:24
oh it was the opposite :P
mniip 2017-02-04 18:49:38
afraid not
erisco 2017-02-04 18:51:45
you just got K-Lined son
erisco 2017-02-04 18:52:22
jle`, I feel like a name other than "Sing" would be helpful
erisco 2017-02-04 18:52:37
yes it is interesting that the types are singletons but it doesn't so much seem the important thing
wesTT 2017-02-04 18:52:38
sup girls join irc.supernets.org
Pestilence 2017-02-04 18:52:38
sup girls join irc.supernets.org
GrodGod 2017-02-04 18:52:38
sup girls join irc.supernets.org
kriskringle 2017-02-04 18:52:38
sup girls join irc.supernets.org
DioSoft 2017-02-04 18:52:38
sup girls join irc.supernets.org
Guest40015 2017-02-04 18:52:38
sup girls join irc.supernets.org
amsty 2017-02-04 18:52:39
sup girls join irc.supernets.org
jle` 2017-02-04 18:53:02
erisco: singletons are a specific consistent pattern
erisco 2017-02-04 18:53:42
yes but the name is odd to me
jle` 2017-02-04 18:54:12
i think it comes from the fact that each type has only a single inhabitant
erisco 2017-02-04 18:54:29
maybe you didn't get my message :P
jle` 2017-02-04 18:54:36
maybe the netsplit :)
dramforever 2017-02-04 18:54:44
In TH am I supposed to use ExpQ everywhere?
erisco 2017-02-04 18:54:51
I said it is interesting that they are singletons but that doesn't seem to be the most important thing
erisco 2017-02-04 18:55:14
:=/NatEq is also a singleton but that isn't what it is about
erisco 2017-02-04 18:56:45
it is literally about defining a term/type equivalent to a promoted type/kind
erisco 2017-02-04 18:57:05
we just can't give both these definitions at once
erisco 2017-02-04 18:58:36
I tried that :P
mniip 2017-02-04 18:59:04
hmm
jle` 2017-02-04 18:59:08
yeah, a bit annoying. you have to duplicate the definitions
jle` 2017-02-04 18:59:22
that's why the singletons has template haskell to make it a bit smoother
erisco 2017-02-04 19:00:50
or I guess I shouldn't say "equivalent", as that is moreso what the unpromoted definition is
erisco 2017-02-04 19:01:35
I mean we want to inhabit all promoted terms
dramforever 2017-02-04 19:01:50
template haskell
dramforever 2017-02-04 19:02:04
Looks like everything works on 'ExpQ's in TH
erisco 2017-02-04 19:02:28
so, for each promoted term, define a term which has the type of the promoted term
erisco 2017-02-04 19:03:15
and to make that work in Haskell we have to add a little wrapper around it as we cannot actually give two distinct terms the same type
erisco 2017-02-04 19:03:25
(the unpromoted version is still laying about)
erisco 2017-02-04 19:03:49
so that's the Sing/SNat
erisco 2017-02-04 19:04:15
and the simplest way to define these terms is to just copy the same structure
erisco 2017-02-04 19:07:20
jle`, does that sound coherent to you?
jle` 2017-02-04 19:09:19
a bit :o i think i get your idea
lyxia 2017-02-04 19:28:00
dramforever: you can use the constructors which just use Exp, with (>>=)
dramforever 2017-02-04 19:28:39
lyxia: But sometimes I want [| nice $(things like) these |]
dramforever 2017-02-04 19:29:01
and $( ) takes ExpQ, [| |] gives ExpQ
dramforever 2017-02-04 19:29:18
Then I thought, hey it makes sense
dramforever 2017-02-04 19:29:37
because [| |] may need a unique variable name supply
mniip 2017-02-04 19:29:39
but really
mniip 2017-02-04 19:29:44
how do I debug something like this
dramforever 2017-02-04 19:32:28
$(each [| (~! getLine) ++ (~! getLine) |]) splices into ((++) <$> getLine <*> getLine). Sounds good?
dramforever 2017-02-04 19:32:50
It's something I'm working on
dramforever 2017-02-04 19:37:15
Uh, no, the context is like a week away. Ignore that
mniip 2017-02-04 19:40:11
augh
mniip 2017-02-04 19:40:17
this seems to be impossible: class SN s => SN (n :: s -> k)
