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 d
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 els
Not directly. You can, however, make a Trustworthy module that re-exports
the (parts of) the Unsafe ones you want to allow yourself to use.
-Edward
On Sun, Mar 16, 2014 at 12:57 PM, Fabian Bergmark wrote:
> Im using the Hint library in a project where users are able to upload
> and run code. A
I agree that this could collide, see my beginning remark that I believe that
the report should provide a minimal specification how to map modules to
filenames and vice versa.
Anyhoo, I'm not married to this specific suggestion. Carter suggested
"Foo+rst.lhs" on IRC, other options would be "Foo.
Im using the Hint library in a project where users are able to upload
and run code. As I don't want them to do any IO, I run the interpreter
with -XSafe. However, some packages (in my case aeson) are needed and
I therefore tried marking them as trusted with ghc-pkg trust aeson.
This seems to have n
Can we get a little more information on what pandoc is doing? Is there a
documentation link?
In part am wondering if it is possible to have a Foo.hs.md file that pandoc
compiles down to Foo.hs with or without help from GHC.
On Sun, Mar 16, 2014 at 5:56 AM, Merijn Verstraaten
wrote:
> Ola!
>
> I
One problem with Foo.*.hs or even Foo.md.hs mapping to the module name
Foois that as I recall JHC will look for
Data.Vector in Data.Vector.hs as well as Data/Vector.hs
This means that on a case insensitive file system Foo.MD.hs matches both
conventions.
Do I want to block an change to GHC because
The behaviour could be invoked only for lower-case parts, but that may
prove problematic on case-insensitive filesystems like Windows.
On 16/03/2014 13:52, Carter Schonwald wrote:
> Idk, this behavior of doing Data.Vector.lhs seems pretty awesome. I
> actually might start doing that. That ghc al
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 like
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 wi
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 complicate
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
http://www.ha
Idk, this behavior of doing Data.Vector.lhs seems pretty awesome. I
actually might start doing that. That ghc allows that seems pretty darn
awesome. And handy too
On Sunday, March 16, 2014, Merijn Verstraaten
wrote:
> My personal approach would have been to make ghc accept "Foo.*.lhs",
> maint
My personal approach would have been to make ghc accept "Foo.*.lhs",
maintaining a list of potential file format seems arduous and error prone.
Cheers,
Merijn
On Mar 16, 2014, at 14:13 , Joachim Breitner wrote:
> Hi,
>
> Am Sonntag, den 16.03.2014, 13:56 +0100 schrieb Merijn Verstraaten:
>> Con
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 g
I'd rather there be some textual finger print in the module itself that be
be used to signal the literate format. But if there's a Case to be made in
open to it I guess.
On Sunday, March 16, 2014, Joachim Breitner
wrote:
> Hi,
>
> Am Sonntag, den 16.03.2014, 13:56 +0100 schrieb Merijn Verstraate
Hi,
Am Sonntag, den 16.03.2014, 13:56 +0100 schrieb Merijn Verstraaten:
> Cons:
GHC would have to either maintain a possibly long of variants to look
for ([".hs", ".lhs", ".rst.lhs", ".md.lhs", ".svg.lhs", ".docx.lhs"]),
or look for "Foo.*.lhs".
I’d find the latter acceptable, but it should be n
Ola!
I didn't know what the most appropriate venue for this proposal was so I
crossposted to haskell-prime and glasgow-haskell-users, if this isn't the right
venue I welcome advice where to take this proposal.
Currently the report does not specify the mapping between filenames and module
names
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 length-
Am 16.03.2014 11:29, schrieb Henning Thielemann:
Since the unary natural number kind so ubiquituous in examples, is there
a recommended module to import it from, which also contains the
injectivity magic of FromNat1? I cannot see it in:
http://hackage.haskell.org/package/base-4.7.0.0/candidate/
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):
That works, someNatVal was the missing piece.
Now the natural next question is how to perform type-level induction on
Nat. This pa
To answer your second question using GADT-style vectors:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE ScopedTypeVariables #-}
module WithVector where
import Data.Maybe
import Data.Proxy
imp
22 matches
Mail list logo
