(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
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
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-outputdir $OUT -i$OUT -o
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 library
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
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
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
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
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 :: Proxy n))
On 25 November 2014 at 19:34, Richard Eisenberg e...@cis.upenn.edu 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
10 matches
Mail list logo
