On 25 November 2014 at 19:34, Richard Eisenberg wrote:
> If I were you, I would just write `g` using unsafeCoerce in the right spot,
> instead of bothering with all the singletons, which would have to use
> unsafety anyway.
Thanks, I hadn't considered this yet.
Cheers,
Bas
___
Hi Alexander,
Thanks for your answer! This provides a lot of ideas how to proceed.
I'm unsure about the following though:
> lessThen :: KnownNat m => SomeNat -> Proxy m -> Maybe (Proof (n <= m) (Proxy
> n))
> lessThen (SomeNat p) k
>| natVal p <= natVal k = Just (Proof $ Tagged (Proxy :: Pr
In my tests, using calloc from:
https://hackage.haskell.org/package/missing-foreign-0.1.1/docs/Foreign-Marshal-MissingAlloc.html
was about twice as fast as allocating and zeroing the same amount of
memory with `newByteArray` + any of `copy/set/fillMutableByteArray`
(all three were nearly ide
We are pleased to announce the first release candidate for GHC 7.8.4:
https://downloads.haskell.org/~ghc/7.8.4-rc1/
This includes the source tarball and bindists for 64bit Linux. Binary
builds for other platforms will be available shortly. These binaries
and tarballs have an accompanying SHA2
Hi, Richard, Bas.
Maybe I didn't spell it properly but my point was to create a data
type that carry a proof
without exposing it's constructor and having clever constructor only,
then the only place
where you need to check will be that constructor.
Also it's possible to write in slightly clearer,
Hi Bas,
I believe to do this "right", you would need singleton types. Then, when you
discover that the number is bounded by 255, you would also discover that the
type is bounded by 255, and you'd be home free.
Unfortunately, I there isn't currently a way to do comparison on GHC.TypeLits
Nats w
> the only reason you do these in individual steps is that you need to
> pass different flags, or are there other reasons?
Not only that – we also want to be able to distinguish compilation
errors between "caused by students" and "we broke something". Under the
assumption that compilation for libr
Dear Lars,
Am Dienstag, den 25.11.2014, 10:36 +0100 schrieb Lars Hupel:
> The invocation is similar to this:
>
> ghc -c -outputdir "$OUT" -XTrustworthy Library.hs
> ghc -c -outputdir "$OUT" -i"$OUT" -XSafe "$SUBMISSION"
> ghc -c -outputdir "$OUT" -i"$OUT" Test_Suite.hs
> ghc-outputd
Hi,
Following approach can work, the idea is to define a type that will
carry a proof (constraint) that we want to check. Here I have reused
Data.Tagged, but it's possible to introduce your own with concrete
constraints.
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeOpe
(cross-posted from [haskell-cafe])
Hi,
I've got a problem in our – admittedly complex – build process. We're
running an automated grading system for student-submitted homework
exercises. The compilation proceeds in stages:
1) Compile a library file, marked as trustworthy
2) Compile student submi
10 matches
Mail list logo
