Hi Henning,
I see two separate issues that show in what you describe, so it might be
useful to discuss them separately:
1. The first issue is figuring out that `n + 1` is always at least 1. As
others have mentioned, GHC currently only does proofs by evaluation,
which is why it gets stuck here.
Hi Iavor,
Am 19.03.2014 22:27, schrieb Iavor Diatchki:
I see two separate issues that show in what you describe, so it might be
useful to discuss them separately:
Thank you and Richard Eisenberg for the detailed explanations. For now,
I have just fooled GHC by unsafeCoerceing dictionaries
Would it be correct to think of closed type families as being more like a
closed, ordered collection of unification queries against the constraint
solver, that happens to act like pattern matching? Does that mean that one
possible but potentially ill advised generalization be some sort of way to
I wouldn't call them unification queries against the constraint solver, because
that implies a little more intelligence than is really there. They are
unification queries, I suppose, against the fully-simplified (i.e., with as
many type family simplifications as possible) arguments.
Pattern
hrm, good point, that helps me understand this better, Thanks!
On Tue, Mar 18, 2014 at 12:25 PM, Richard Eisenberg e...@cis.upenn.eduwrote:
I wouldn't call them unification queries against the constraint solver,
because that implies a little more intelligence than is really there. They
are
On Sun, Mar 16, 2014 at 11:06 AM, Christiaan Baaij
christiaan.ba...@gmail.com wrote:
Iavor is working on a branch that allows the constraint solver to call an
external solver: https://github.com/ghc/ghc/tree/decision-procedure
Currently, it: a) only supports CVC4 (an SMT solver), and b) is
So much to respond to!
First, a little relevant context: Iavor Diatchki is the primary implementor of
the type-lits stuff; I am not. But, he and I are playing in the same
playground, so to speak, so we confer a fair amount and I may have some helpful
perspective on all of this.
Henning asks:
(aside, pardon my earlier tone, been a bit overloaded the past few weeks,
that crossed over to the list)
OOO
that works?
I guess that gives a decent way of using TypeLits as a concrete input
syntax for Peano numbers. Thanks for pointing that out
I think i'm gonna go drop 7.6 support on some code
Am 16.03.2014 09:40, schrieb Christiaan Baaij:
To answer the second question (under the assumption that you want
phantom-type style Vectors and not GADT-style):
Now I like to define non-empty vectors. The phantom parameter for the
length shall refer to the actual vector length, not to
You can't with type lits. The solver can only decide concrete values :(
You'll have to use a concrete peano Nats type instead.
I've been toying with the idea that the type lits syntax should be just
that, a type level analogue of from integer that you can give to user land
types, but I'm not
Am 16.03.2014 13:48, schrieb Dan Frumin:
This is just a wild guess, but is there a possibility that (1+n) will
produce less complaints than (n+1)?
unfortunately no
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
Am 16.03.2014 14:35, schrieb Carter Schonwald:
You can't with type lits. The solver can only decide concrete values :(
I hoped that with type-level natural numbers all my dreams would become
true. :-)
I'd be also happy if I could manually provide the proof for 1=n+1 and
more complicated
its a special Thing that just uses Integer internally, but because it
doenst provide a PEANO api, we can't do computations on it :'(
On Sun, Mar 16, 2014 at 10:37 AM, Henning Thielemann
lemm...@henning-thielemann.de wrote:
Am 16.03.2014 14:35, schrieb Carter Schonwald:
You can't with
Iavor is working on a branch that allows the constraint solver to call an
external solver: https://github.com/ghc/ghc/tree/decision-procedure
Currently, it: a) only supports CVC4 (an SMT solver), and b) is slightly
out of of line with HEAD.
I think the above branch will be able to solve things
respectfully,
The current typeLits story for nats is kinda a fuster cluck to put it
politely . We have type lits but we cant use them (well, we can't compute
on them, which is the same thing).
For the past 2 years, every ghc release cycle, I first discover, then have
to communicate to everyone
Am 16.03.2014 20:02, schrieb Carter Schonwald:
respectfully,
The current typeLits story for nats is kinda a fuster cluck to put it
politely . We have type lits but we cant use them (well, we can't
compute on them, which is the same thing).
For the past 2 years, every ghc release cycle, I first
16 matches
Mail list logo
