erisco 2017-02-03 17:49:08
I can say 0 < S n but Haskell obviously still has no idea what is going on
mniip 2017-02-03 17:50:48
0 < S n is an axiom
mniip 2017-02-03 17:50:54
you could define < as a tyclass
erisco 2017-02-03 17:51:03
yes it is given to me
mniip 2017-02-03 17:51:04
or as a tyfam
erisco 2017-02-03 17:51:10
I am saying I can bring it in scope but this doesn't help
mniip 2017-02-03 17:51:14
with that as a rul
mniip 2017-02-03 17:51:14
e
erisco 2017-02-03 17:53:31
when is Haskell actually going to know a case is impossible
erisco 2017-02-03 17:54:00
I don't know what kind of evidence would ever work
erisco 2017-02-03 17:55:01
if it cannot figure out 'S n ~ 'Z never succeeds then what else could I possibly do
erisco 2017-02-03 17:55:11
they are plainly stated as a data type
erisco 2017-02-03 17:55:35
'S and 'Z are distinct constructors of the same lifted type... it should be obvious!
erisco 2017-02-03 18:00:04
I figured out the problem folks
erisco 2017-02-03 18:00:43
my code was wrong :)
erisco 2017-02-03 18:01:07
http://lpaste.net/352076 there we go
erisco 2017-02-03 18:01:35
I was taking Sing n and Sing m instead of Sing ('S n) and Sing ('S m)
erisco 2017-02-03 18:01:47
which was giving me the wrong proposition
Jinixt 2017-02-03 18:04:04
if one were to implement a compiler in haskell, is there a way to piggyback on GHC's type inference system? (with my own compiler's types)
erisco 2017-02-03 18:08:22
well the typical way to do this is with an eDSL
erisco 2017-02-03 18:08:40
if you mean to rip out pieces of GHC to use in your own compiler, I dunno
Jinixt 2017-02-03 18:09:59
the source language isn't haskell so it'd have to be the latter
erisco 2017-02-03 18:11:39
how am I supposed to get an IsTrue (a :< b), bleh
erisco 2017-02-03 18:11:57
you can construct Leq proofs but there is no Lneq
erisco 2017-02-03 18:13:17
I have (n :< m) ~ True in context but there is no conversion
jle` 2017-02-03 18:16:25
i think you should be able to just use the Witness constructor
erisco 2017-02-03 18:16:57
hm, I suppose that makes sense
erisco 2017-02-03 18:17:18
Witness :: IsTrue P where P is whatever my problem is
jle` 2017-02-03 18:17:45
you can use 'Witness :: IsTrue p' whenever (p ~ True) is in your context
jle` 2017-02-03 18:17:47
yeah
erisco 2017-02-03 18:18:30
a bit mind bending for me at the moment
jle` 2017-02-03 18:18:36
so if you have `(n :< m) ~ True` in your context, you can use 'Witness :: IsTrue (n :< m)'
erisco 2017-02-03 18:18:51
yes, right
jle` 2017-02-03 18:18:58
to get a value of IsTrue (n :< m)
jle` 2017-02-03 18:19:07
*of type
erisco 2017-02-03 18:23:13
I expect there to be a way to do substitution... so IsTrue (n :~: n') -> IsTrue (n :<= m) -> IsTrue (n' :<= m)
erisco 2017-02-03 18:23:49
maybe I have to make that lemma as well
erisco 2017-02-03 18:25:49
or maybe I just bring the equality into the context and work it that way? maybe so
dmwit 2017-02-03 18:37:05
Jinixt: GADTs are essentially a way to embed your language's type system into Haskell.
Jinixt 2017-02-03 18:38:35
dmwit: and this would give me "free" type inference? got any good resources for this?
Jinixt 2017-02-03 18:39:08
i haven't really used GADTs before
dmwit 2017-02-03 18:39:32
http://www.monoidal.net/papers/qhaskell.pdf shows how to use GADTs + typeclasses to embed a linearly typed language into Haskell and get inference on it.
Jinixt 2017-02-03 18:39:40
thanks!
