- Haskell-Cafe - Haskell.org

Caching functions compiled with llvm-hs
by Tom Westerhout 12 Jul '20

12 Jul '20

Hello, Suppose I've written some function f :: Foo -> Bar using LLVM IR. Now I'd like to compile it on first invocation with llvm-hs and cache the obtained function pointer. Basically something like this f :: Foo -> Bar f x = fImpl x where fImpl = unsafePerformIO $ flag <- isAlreadyCompiled -- check the cache if flag fetchFunc -- get the compiled code from cache else compileWithLLVM -- build LLVM IR, compile it, and update the cache A very primitive JIT compiler. What is the best way to do this with llvm-hs? All standard examples using LLVM.OrcJIT or LLVM.ExecutionEngine show how to compile a function and then immediately execute it. I can't quite figure out a safe way to keep the FunPtr... Big code bases like Accelerate or JuliaLang do achieve this somehow, but are quite difficult to understand for the uninitiated. Any advice is highly appreciated! Cheers, Tom

2 2

Re: [Haskell-cafe] Test on identity?
by Olaf Klinke 11 Jul '20

11 Jul '20

> Am 09.07.20 um 20:26 schrieb Olaf Klinke: > > Joachim Durchholz wrote: > >> This "identity is equality under change" definition captures not > >> just > >> two objects at identical addresses, but also proxies, network > >> objects, > >> files, and whatever there is. > >> > >> Step 3: Realize that if you have an immutable object, there is no > >> relevant difference between equality and identity anymore. (You > can > >> make > >> various formal statements about this.) > > > > Is that what is called "extensional equality"? Values a,b :: A are > > extensionally equal if they behave the same in all contexts. > > To fully treat this, you have to explore some pretty interesting > waters. > > First, "all contexts" can mean pretty different things. > E.g. in Haskell (without unsafe* and similar), everything is > immutable, > so you have contexts that exist in languages with mutability but not > in > Haskell, and you'd have to define what "all contexts" means for a > general term like "extensional equality". > > Second, "behave the same" means that for all functions, the result it > equal. > That's a recursive definition. You need fixed-point theory to turn > that > statement into an actual definition. > And that's surprisingly tricky. > > One fixed point is to say "the largest set of equal objects", which > means everything is equal to everything - fits the above definition > (applying any function to anything will trivially return results > that > are equal under this definition), but is obviously not what we > wanted. > > Another one would be to have what we'd intuitively define as > equality. > Say, in Haskell, the minimum set of equalities that makes different > constructor calls unequal. (Plus a handful of clerical definitions > to > catch special cases like integers.) > > Another one would be to have what we'd intuitively define as > identity. > > Plus various other fixed points. > > For example, consider proxies - say, an object that talks to a > remote > machine to produce its function results. > Now if you assume a proxy for integer values, is the proxy equal to > an > arbitrary integer you may have locally? > Again, this depends on what fixed point you choose for your equality > definition. You can define that as an exception, you consider two > objects equal if their functions return equal results, except for > those > that inspect the proxy-specific state; then proxy and local value > are > equal. Or you don't make an exception, then the two are not equal. > From a mathematical standpoint, either fixed point will satisfy the > above recursive definition (definition template, if you will). From > a > computing standpoint, you'll find that depending on context, you > want > one or the other! > > There are different types of proxy objects, and you can have > different > kinds of equality depending on how you treat them. > > That multitude of equality functions is pretty useless in a > programming > context; nobody wants to mentally deal with a gazillion of subtly > different equalities! > So I belive what one should do in practice is to have converter > functions. E.g. one that turns an Int proxy into an Int, merely by > stripping the proxy-specific functions. > That keeps the special cases to the place where they belong - all > those > types that have funky special kinds of equality. > Mutable data is another case of this. The equality of a mutable > object > can be defined as identity, and a converter function returns an > immutable copy so that equality is what's usually considered "value > equality" (equals() in Java). > (Languages that do not cleanly separate mutable and immutable types > will > still have to deal with two equalities, value equality and > identity... > well, the above is type and language design theory, practical > languages > are always a set of trade-offs, restricted by the limited knowledge > and > experience of the language designer. I guess that's why we have so > many > programming languages.) > I find it easier to intuitively define what extensional inequality means: As a domain theorist I declare two values unequal if there is an open set (a semi-decidable property) containing one but not the other value. For pure types t (not involving IO) that means there is a function semidecide :: t -> () that returns () for the one value and bottom for the other. I can not say how this would extend to impure types and I tend to agree with you that the notion of equality then depends on the intended semantics. Below the semidecision would have type t -> I0 () However, using StableName (thanks, Zemyla and Viktor!) indeed one is able to detect sharing. It works only after forcing the values, though. Apparently StableName does not work on thunks. Olaf ghci> import System.Mem.StableName ghci> import Control.Applicative ghci> data Ex = Val Int | Add Ex Ex deriving (Show) ghci> a = Add (Val 1) (Val 1) ghci> b = let v = Val 1 in Add v v ghci> show a "Add (Val 1) (Val 1)" ghci> show b "Add (Val 1) (Val 1)" ghci> let f :: Ex -> IO Bool; f (Val _) = return False; f (Add x y) = liftA2 eqStableName (makeStableName x) (makeStableName y) ghci> f a False ghci> f b True

1 0

Re: [Haskell-cafe] Test on identity?
by Johannes Waldmann 10 Jul '20

10 Jul '20

> Stable names are great! ... > I think they’re also used in eds ersatz package sortah. Yes. This is the package https://hackage.haskell.org/package/ersatz This is where they are used https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Problem.hs#L149 - J.W.

1 0

Re: [Haskell-cafe] Test on identity?
by Olaf Klinke 10 Jul '20

10 Jul '20

Joachim Durchholz wrote: > This "identity is equality under change" definition captures not > just > two objects at identical addresses, but also proxies, network > objects, > files, and whatever there is. > > Step 3: Realize that if you have an immutable object, there is no > relevant difference between equality and identity anymore. (You can > make > various formal statements about this.) Is that what is called "extensional equality"? Values a,b :: A are extensionally equal if they behave the same in all contexts. That is, there is no type X and no function f :: A -> X such that f a can be observed to be different from f b, e.g. f a throws an exception and f b does not, or X is in Eq and f a /= f b. Can one write a function (even using reallyUnsafePtrEquality#) that distinguishes the following? a = Add (Val 1) (Val 1) b = let v = Val 1 in Add v v I tried: import GHC.Exts peq :: a -> a -> Bool peq x y = I# (reallyUnsafePtrEquality# x y) == 1 f :: Ex -> Bool f (Val _) = False f (Add x y) = peq x y But I get (even when I make the fields of Add strict): peq a a == True f a == False f b == False Olaf

5 4

Linking + zstd on FreeBSD
by Vanessa McHale 09 Jul '20

09 Jul '20

I tried linking against zstd within a Vagrant simulating FreeBSD. I get the following: ld: error: duplicate symbol: XXH64 >>> defined at xxhash.c >>> xxhash.o:(XXH64) in archive /home/vagrant/.cabal/store/ghc-8.8.3/zstd-0.1.2.0-c8ee757c8e8a7307779ab3cfbc91f3445940e16bbf8f9916f4c90432a0ac499e/lib/libHSzstd-0.1.2.0-c8ee757c8e8a7307779ab3cfbc91f3445940e16bbf8f9916f4c90432a0ac499e.a >>> defined at xxhash.c:693 (/wrkdirs/usr/ports/lang/ghc/work/ghc-8.8.3/rts/xxhash.c:693) >>> RTS.o:(.text.XXH64+0x0) in archive /usr/local/lib/ghc-8.8.3/rts/libHSrts.a ... I am using GHC version 8.8.3_1 and cabal-install 3.0 installed by 'sudo pkg install ...' (I was trying to run cabal install language-dickinson) Cheers, Vanessa McHale

4 6

Re: [Haskell-cafe] Test on identity?
by Olaf Klinke 08 Jul '20

08 Jul '20

> Dear Café, > > I'm trying to build a DAG from a binary tree. I don't think there's a > big trouble. > Nevertheless, I do even some transformations. Thus, I would like to > know it is still a > DAG, not adding, accidentally, a node. > > Is there any way, if I have data like > > data Ex > = Val Int > | Add Ex Ex > > so that I can test that some value Val i === Val i ? I mean, the > pointers go to the > same data box? I could do that via some IORefs, AFAIK, but I don't > think it is > feasible. Maybe to tune the algorithm... > > Best regards, > > Dusan So the binary tree is a value e :: Ex, right? And the DAG (directed acyclic graph) is an explicit representation of the internal pointer structure in e? Did I understand you right? This sounds like you should represent Ex as a fixed point and then invoke some fixed point magic like catamorphisms. Your transformation might have to be re-written as a cata/ana/hylomorphism, too. Below is a recipe to turn any element of any fixed point type into a graph, that is, into a list of nodes and edges. Of course this will loop if your data was not a finite DAG, e.g. due to self-reference. -- make type recursion for your type Ex explicit data ExF x = Val Int | Add x x deriving (Show) instance Functor ExF where fmap f (Val i) = Val i fmap f (Add x y) = Add (f x) (f y) instance Foldable ExF where foldMap _ (Val _) = mempty foldMap f (Add x y) = f x <> f y instance Traversable ExF where traverse f (Val i) = pure (Val i) traverse f (Add x y) = Add <$> (f x) <*> (f y) -- represent Ex via the general -- Fix :: (* -> *) -> * -- See e.g. package data-fix or recursion-schemes -- cataM below taken from the data-fix package type Ex = Fix ExF -- = Fix {unFix :: ExF (Fix ExF)} -- Add () () tells you the node is internal type ExNode = ExF () data GraphElem f = Node Int (f ()) | Edge Int Int instance Show (GraphElem ExF) where show (Node n (Val i)) = show n ++ ":Val " ++ show i show (Node n (Add _ _)) = show n ++ ":Add" show (Edge i j) = show i ++ " -> " ++ show j type Graph = [GraphElem ExF] type GraphM = StateT Int (Writer Graph) structure :: (Traversable f, MonadState Int m, MonadWriter [GraphElem f] m) => f Int -> m Int structure fi = do this <- get tell [Node this (void fi)] traverse (\child -> tell [Edge this child]) fi put (this+1) return this -- depth-first traversal. More generally dag has type -- (Traversable f) => Fix f -> [GraphElem f] -- and the Traversable instance determines the order -- of the traversal. dag :: Ex -> Graph dag = snd . runWriter . flip evalStateT 0 . cataM structure -- Cheers, Olaf

1 0

Test on identity?
by Dušan Kolář 08 Jul '20

08 Jul '20

Dear Café, I'm trying to build a DAG from a binary tree. I don't think there's a big trouble. Nevertheless, I do even some transformations. Thus, I would like to know it is still a DAG, not adding, accidentally, a node. Is there any way, if I have data like data Ex = Val Int | Add Ex Ex so that I can test that some value Val i === Val i ? I mean, the pointers go to the same data box? I could do that via some IORefs, AFAIK, but I don't think it is feasible. Maybe to tune the algorithm... Best regards, Dusan

4 4

FMBC 2020 - Call for Participation
by Bruno Bernardo 07 Jul '20

07 Jul '20

[ Please distribute, apologies for multiple postings. ] ======================================================================== 2nd Workshop on Formal Methods for Blockchains (FMBC) 2020 - Call for Participation https://fmbc.gitlab.io/2020 July 20 and 21, 2020, Online, 6AM-8AM PDT Co-located with the 32nd International Conference on Computer-Aided Verification (CAV 2020) http://i-cav.org/2020/ --------------------------------------------------------- The FMBC workshop is a forum to identify theoretical and practical approaches of formal methods for Blockchain technology. Topics include, but are not limited to: * Formal models of Blockchain applications or concepts * Formal methods for consensus protocols * Formal methods for Blockchain-specific cryptographic primitives or protocols * Design and implementation of Smart Contract languages * Verification of Smart Contracts The list of lightning talks and conditionally accecpted papers is available on the FMBC 2020 website: https://fmbc.gitlab.io/2020/program.html There will be one keynote by Grigore Rosu, Professor at University of Illinois at Urbana-Champaign, USA and Founder of Runtime Verification. Registration Registration to FMBC 2020 is free but required. It is done through the CAV 2020 registration form: http://i-cav.org/2020/attending/ Please register before *July 10, 2020*.

1 0

ekg-core/RTS : bogus GC stats when running on Google Cloud Run
by Marco Zocca 04 Jul '20

04 Jul '20

Hi all, I have two services deployed on Google cloud infrastructure; Service 1 runs on Compute Engine and Service 2 on Cloud Run and I'd like to log their memory usage via the `ekg-core` library (https://hackage.haskell.org/package/ekg-core-0.1.1.7/docs/System-Metrics.ht…) (which is just a thin wrapper around GHC.Stats ). The logging bracket is basically this : mems <- newStore registerGcMetrics mems void $ concurrently io (loop mems) where loop ms = do m <- sampleAll ms ... (lookup the gauges from m and log their values) threadDelay dt loop ms I'm very puzzled by this: both rts.gc.current_bytes_used and rts.gc.max_bytes_used gauges return constant 0 in the case of Service 2 (the Cloud Run one), even though I'm using the same sampling/logging functionality and build options for both services. This is about where my knowledge ends; could this behaviour be due to the Google Cloud Run hypervisor ("gRun") implementing certain syscalls in a non-standard way (gRun syscall guide : https://gvisor.dev/docs/user_guide/compatibility/linux/amd64/) ? Thank you for any pointers to guides/manuals/computer wisdom. Details : Both are built with these options : -optl-pthread -optc-Os -threaded -rtsopts -with-rtsopts=-N -with-rtsopts=-T the only difference is that Service 2 has an additional flag -with-rtsopts=-M2G since Cloud Run services must work with 2 GB of memory at most. The container OS in both cases is Debian 10.4 ("Buster").

1 1

Is there a handy refl or refl generator for converting GADT types?
by chris done 02 Jul '20

02 Jul '20

Hi all, I have stages in my compiler that convert e.g. Global Renamed -> Global Generated, etc. where certain constructors are available in certain stages. data GlobalRef s where FromIntegerGlobal :: GlobalRef s FromDecimalGlobal :: GlobalRef s InstanceGlobal :: !InstanceName -> GlobalRef Resolved E.g. after type class resolution is done, the InstanceGlobal constructor is available. But instances can't appear in the AST at other stages. In three stages, I've had to copy/paste this code: + refl = + case name of + FromIntegerGlobal -> FromIntegerGlobal + FromDecimalGlobal -> FromDecimalGlobal Because if I just put `name` then GHC will complain that the types are different, which is correct. But a straight-forward pattern match gives GHC the proof that they can be converted. Is there a handy way already implemented that could derive either this code or this proof for me? Cheers, Chris

3 3