compiling-to-categories / concat Goto Github PK
View Code? Open in Web Editor NEWCompiling to Categories
Home Page: http://conal.net/papers/compiling-to-categories
License: BSD 3-Clause "New" or "Revised" License
concat's People
Contributors
Stargazers
Watchers
Forkers
josephjohncox cartazio silky capn-freako luke-clifton strake paddymahoney aakarsh julian-becker keithschulze tavakyan cfhammill abailly well-typed kosmikus wygulmage totbwf ugeorge soraismus phischu fuath jrp2014 kenranunderscore eschnett cmk sellout guibou daheath stjordanis dbeacham templatek mikesperber faezs active-group tristancacqueray mjepronk zliu41 micahscopes freckletonj maxdiefenbach con-kitty srid mkovaxx paulroden cxandru thongpv87 vnredmon fmorgnerconcat's Issues
what is the current status of support for recursive definitions?
we chatted about how thats current a no go at ICFP 2017, has there been any action on that since?
concat-plugin sometimes generates "Failed to load interface for ... hidden module"
The presence of imports sometimes causes ccc to try to load hidden modules, which causes compilation to fail. For example, this module:
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fplugin=ConCat.Plugin -fplugin-opt ConCat.Plugin:trace #-}
module LoadsHiddenModule where
import ConCat.AltCat
import qualified Data.Aeson
f :: a -> a
f = ccc @(->) (\x -> x)will produce output like this:
[1 of 1] Compiling LoadsHiddenModule ( LoadsHiddenModule.hs, LoadsHiddenModule.o )
go ccc (->): \ (x_adEQ :: a_adF0) -> x_adEQ :: a_adF0 -> a_adF0
Doing lam Id
user error (Errors:
<interactive>:1:1: error:
Failed to load interface for ‘Data.Attoparsec.Text.Internal’
it is a hidden module in the package ‘attoparsec-0.13.1.0’
Use -v to see a list of the files searched for.
Warnings:)
However, if the import qualified Data.Aeson is removed, compilation will succeed and work as expected.
Deduplicate LoopCat and TracedCat
It was pointed out on the FP slack that both of these classes exist in ConCat.Category, but are defined identically.
It seems like either the difference should be documented or one should be removed. Considering that the implementation of TracedCat (->) is the same as ArrowLoop (->), I'm assuming they're actually the same, in which case the preferred name just needs to be decided. I'm partial to TracedCat, as it's from CT and has better implementations already, but LoopCat matches the Haskell naming (ArrowLoop) and, judging by them being added in the same commit, perhaps has some relationship to DelayCat?
There's also a missing TracedCat (Constrained con k) instance which should be added.
I'm happy to do the work once I know which name is preferred.
Interview partners for research about communication in GitHub projects wanted
Hi. My name is Verena Ebert, and I am a PhD student at the University of Stuttgart in Germany.
A few months ago, I have examined 90 GitHub projects to see what communication channels they use and how they write about them in the written documents, for example README or wiki. If you are interested in the previous results, you can find them here:
https://arxiv.org/abs/2205.01440
Your project was one of these 90 projects and, therefore, I am interested in further details about your communication setup.
To gather more data about your communication setup, I kindly ask one of the maintainers to do an interview with me. The interview will be about 30-35 minutes long and via Skype, WebEx or any other provider you prefer. The interviews should be done in November 2022, if possible.
In this interview, I would like to ask some questions about the reasons behind the channels, to understand the thoughts of the maintainers in addition to the written information.
The long goal of my PhD is to understand how communication works in GitHub projects and how a good set of communication channels and information for other maintainers and developers looks like. One possible outcome is a COMMUNICATION.md with instructions and tips about which channels could be useful and how these channels should be introduced to other projects participants. Of course, if you are interested, I will keep you up to date about any further results in my research.
If you are interested in doing an interview, please respond here or contact me via email ([email protected]). We will then make an appointment for the interview at a time and date that suits you.
If you agree, I would like to record the interview and transcribe the spoken texts into anonymized written texts. In this case, I will send you the transcript for corrections afterwards. Only if you agree, the transcripts or parts of it would be part of a publication.
Publish (parts of) concat on Hackage?
I'm curious if @conal is interested in this at all and, if so, what are any issues standing in the way of it.
For our purposes, we only care about concat-classes and concat-examples being published (although this implies all their deps are published).
There are two things I'd like to see change before concat-examples is published, though:
- its tests shouldn't require human interaction (all the graphviz windows need to be closed for the test to complete) and
- it shouldn't depend on concat-plugin (moving the tests to concat-plugin would solve both of these, I suppose).
I'm happy to do the work to get this to happen if there's interest.
Ok type family with second argument
Try making the associated Ok constraint depend on the object/type parameter as well as the category, and eliminate classes introduced to accommodate the current single-parameter dependency. See Make the Obj' type family depend on object as well as category.
Rebox rules violate ghc invariant
When running plugin output through -dcore-lint, we currently may get something like this:
*** Core Lint errors : in result of Simplifier ***
Bar.hs:25:1: warning:
This argument does not satisfy the let/app invariant:
case plus (I# 10#) (I# 1#) of { I# i#_aBa -> i#_aBa }
In the RHS of foo :: Int
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
This is because the reboxing rules are shaped like this:
rebox2" [~0] (+#) = \ u# v# -> unboxI (addC (boxI u#, boxI v#))
This rewrites, for instance, 10# +# 1# into case plus (I# 10#) (I# 1#) of { I# i#_aBa -> i#_aBa }). While the former is ok-for-speculation, the latter is not. (The lint error message might be different, but comes down to the same cause.)
See https://gitlab.haskell.org/ghc/ghc/-/issues/18677 for SPJ's take on this.
Now, the paper has an older version of these rules, which do not have this problem. This is preserved in Rebox.hs but #ifdefed out here:
Switch to quantified constraints, and eliminate entailment logic
Now that GHC has quantified constraints, the tedious constraint entailment logic can probably be eliminated from the implementation. See a similar conversation.
Too much inlining
When we uncomment this line:
https://github.com/conal/concat/blob/master/examples/test/Examples.hs#L421
i.e. this one:
runCirc "affRelu" $ toCcc $ affRelu @(Vector 2) @(Vector 3) @R
The plugin fails to transform the toCCC away. Looking at the plugin output, it appears the problem is that the runCirc gets inlined to an insane amount of IO-related code: Without the call to runCirc, it works fine.
Unfortunately, turning the INLINE annotation for runCirc into NOINLINE doesn't change anything - the inlining still happens.
Plugin diverges on function composition
The following call does not terminate:
(toCcc (\f g x -> f (g x)))
When enabling the trace, one sees that the generated term gets larger and larger.
Idea: Backward propagation
We can hopefully get backward propagation using
newtype F a b = F (a -> ( b :* (b -> a) ))
We can add that to the two existing ADs. I'm not sure how to make it Closed though; it seems that you can't.
Constructing a graph of RLC circuit elements and transforming to an affine relation between inputs and outputs.
Hi Conal,
This is more of a general design guideline question than an issue, but I don't know of a more appropriate forum so I'm asking here.
I've been trying to implement the formalism of cospan composition following along with https://arxiv.org/abs/1707.08321 to construct a "blackbox functor" semantics that maps a labelled graph of circuit elements (passive linear + current and voltage sources) to the affine map between inputs and outputs attached to the terminals.
Probably due to my inadequacy in both haskell and CT, I've taken several routes such as trying to construct the hypergraph category LCirc (symmetric monoidal with a frobenius algebra) myself but going by the SMT example I'm now thinking it might be more appropriate to use the primitives you export in the Circuit module to do the construction.
What I would appreciate your guidance on is the process of giving the mapping from this circuit representation to an affine map the semantics dictated by Kirchoff's laws - if I were to naively just construct a Sum type for the set of circuit elements and declare a GenBuses instance for them and write an evaluator that has similar constraints on the domain as the ones you choose in the SMT module, how would I go from (RLC :> RLC) -> Affine R RLC RLC?
And thank you so much for your work, it has been mind-bending and invigorating in the best ways!
tracing output incoherent while multiple modules are building
found this gem in my terminal
@ a
(subC @ (->) @ Double ($fNumCat(->)a @ Double $fNumDouble))
(irred1
`cast` (Sub (D# 1.0## (D:R:Ok:**:[0] <Syn>_N <(:>)>_N) <a>_N
)
r1
:: Cont: Stop[RhsCtxt] R
(Ok (Syn :**: (:>)) a :: Constraint)
~R#
((&+&) (Ok Syn) (Ok (:>)) a :: Constraint))),
Rule fired
$p1&+&
Rule: rebox2
Module: @ (ConCat.Rebox)
Before: *
/## ValArg 1.0## ValArg@ y
After: (Ok Syn)
let @ (Ok (:>))
{
$dFractionalCat ::@ b
FractionalCat (->) Double
$dFractionalCat
= $fFractionalCat(->)a @ Double $fFractionalDouble } in
(irred
\ `cast` (Sub (u# :: Double#) (v# :: (D:R:Ok:**:[0] <Syn>_N <(:>)>_N) <b>_N
Double#) ->
:: unboxD (divideC @ (->) @ Double $dFractionalCat (boxD u#, boxD v#))
Cont: Select nodup wild4
(Ok (Syn :**: (:>)) b :: Stop[BoringCtxt Constraint)
] Bool
~R#
((&+&) (Ok Syn) (Ok (:>)) b :: Constraint))))
Stop[BoringCtxtRule fired
Rule:] Syn (Prod Syn a b) a
rebox2
GHC panic
Not sure if this is the appropriate place, but there seems to be a problem with GHC 8.0.2 and the latest code. When building concat-examples, GHC crashes with the following error message:
[1 of 1] Compiling Main ( test/Examples.hs, .stack-work/dist/x86_64-osx/Cabal-1.24.2.0/build/examples/examples-tmp/Main.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-apple-darwin):
ccc
lam Unhandled \ (eta_ds_Bh
:: ((R -> Double, R), (R -> Double, R))) ->
case deriv
@ (->)
@ R
@ Double
(exl
@ (->)
@ (R -> Double)
@ R
$fProductCat(->)
(($fYes1ka @ * @ (R -> Double), $fYes1ka @ * @ Double)
`cast` ((Sym R:Ok(->)[0] <Double -> Double>_N,
Sym R:Ok(->)[0] <Double>_N)_R
:: ((Yes1 (Double -> Double), Yes1 Double) :: Constraint)
~R#
((Ok (->) (Double -> Double),
Ok (->) Double) :: Constraint)))
(exl
@ (->)
@ (R -> Double, R)
@ (R -> Double, R)
$fProductCat(->)
(($fYes1ka @ * @ (R -> Double, R), $fYes1ka @ * @ (R -> Double, R))
`cast` ((Sym R:Ok(->)[0] <(Double -> Double, Double)>_N,
Sym R:Ok(->)[0] <(Double -> Double, Double)>_N)_R
:: ((Yes1 (Double -> Double, Double),
Yes1 (Double -> Double, Double)) :: Constraint)
~R#
((Ok (->) (Double -> Double, Double),
Ok (->) (Double -> Double, Double)) :: Constraint)))
eta_ds_Bh))
of wild_00 {
}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Progress: 22/23
-- While building package concat-examples-0.3.0.0 using:
/Users/chris/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_1.24.2.0_ghc-8.0.2 --builddir=.stack-work/dist/x86_64-osx/Cabal-1.24.2.0 build lib:concat-examples test:examples --ghc-options " -ddump-hi -ddump-to-file"
Process exited with code: ExitFailure 1
Generates too many nodes, sometimes.
@conal as we discussed at LambdaJam, I've collected an example where the circuit generates more nodes than it needs to, along with the modifications required to convince the output to be in the form I desired (fewer nodes).
https://github.com/luke-clifton/concat/blob/shrinkable/test/Examples.hs#L184 generates the following
when I would really rather it generated this.
Which was actually generated by the following.
https://github.com/luke-clifton/concat/blob/shrinkable/test/Examples.hs#L192
Make it easier to modify and run the test suite
I was trying out the library so was looking at the test suite for some examples about how to get started. Unfortunately, I can't work out how to run most of the tests as you have to select the right CPP flag for whichever commented out tests you want to run.
Choosing object definitions in categories
I'm trying to represent the Z3 Monad as a Kleisli category, because I'd love to write solver equations using simple, boolean+numeric Haskell functions. However, booleans and other types in Z3 are
not distinguished objects in that category: There is only one object, AST, with all morphisms being endomorphisms on that object.
error compiling all examples
I'm trying to experiment with the library. Howerer, I can't get it to compile.
🌙 [master*]$ stack build :graphics-examples
concat-graphics-0.1.0.0: configure (lib + test)
Configuring concat-graphics-0.1.0.0...
clang: warning: argument unused during compilation: '-nopie' [-Wunused-command-line-argument]
concat-graphics-0.1.0.0: build (lib + test)
Preprocessing library for concat-graphics-0.1.0.0..
Building library for concat-graphics-0.1.0.0..
Preprocessing test suite 'graphics-examples' for concat-graphics-0.1.0.0..
Building test suite 'graphics-examples' for concat-graphics-0.1.0.0..
[1 of 1] Compiling Main ( test/Examples.hs, .stack-work/dist/x86_64-osx/Cabal-2.0.1.0/build/graphics-examples/graphics-examples-tmp/Main.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64-apple-darwin):
lam Case of product live wild binder
case exr
@ (->)
@ (R :* R, (R, R) -> Bool)
@ (R, R)
$fProductCat(->)
(($fYes1ka @ * @ (R :* R, (R, R) -> Bool), $fYes1ka @ * @ (R, R))
cast(((%,%)
(Sym (R:Ok(->)[0]) <((Double, Double),
(Double, Double) -> Bool)>_N)
(Sym (R:Ok(->)[0]) <(Double, Double)>_N))_R
:: ((Yes1 ((Double, Double), (Double, Double) -> Bool),
Yes1 (Double, Double)) :: Constraint)
~R#
((Ok (->) ((Double, Double), (Double, Double) -> Bool),
Ok (->) (Double, Double)) :: Constraint)))
w_g_x_Xi
of wild_adaJ
{ (a1_adaL, b1_adaM) ->
case a1_adaL of { D# x1_adaQ ->
case exl
@ (->)
@ R
@ R
$fProductCat(->)
($d(%,%)_XjKg
cast(((%,%)
(Sym (R:Ok(->)[0]) _N) (Sym (R:Ok(->)[0]) _N))_R
:: ((Yes1 R, Yes1 R) :: Constraint)
~R#
((Ok (->) R, Ok (->) R) :: Constraint)))
(exl
@ (->)
@ (R :* R)
@ ((R, R) -> Bool)
$fProductCat(->)
(($fYes1ka @ * @ (R, R), $fYes1ka @ * @ ((R, R) -> Bool))
cast(((%,%)
(Sym (R:Ok(->)[0]) <(Double, Double)>_N)
(Sym (R:Ok(->)[0]) <(Double, Double) -> Bool>_N))_R
:: ((Yes1 (Double, Double),
Yes1 ((Double, Double) -> Bool)) :: Constraint)
~R#
((Ok (->) (Double, Double),
Ok (->) ((Double, Double) -> Bool)) :: Constraint)))
(exl
@ (->)
@ (R :* R, (R, R) -> Bool)
@ (R, R)
$fProductCat(->)
(($fYes1ka @ * @ (R :* R, (R, R) -> Bool), $fYes1ka @ * @ (R, R))
cast(((%,%)
(Sym (R:Ok(->)[0]) <((Double, Double),
(Double, Double) -> Bool)>_N)
(Sym (R:Ok(->)[0]) <(Double, Double)>_N))_R
:: ((Yes1 ((Double, Double), (Double, Double) -> Bool),
Yes1 (Double, Double)) :: Constraint)
~R#
((Ok (->) ((Double, Double), (Double, Double) -> Bool),
Ok (->) (Double, Double)) :: Constraint)))
w_g_x_Xi))
of
{ D# y_adaU ->
case divideC
@ (->) @ Double $s$fFractionalCat(->)a_shqs (lvl_siqO, boxD y_adaU)
of
{ D# d#_af3a ->
case mulC
@ (->) @ Double $s$fNumCat(->)a_shlp (boxD x1_adaQ, boxD d#_af3a)
of
{ D# d#_XfjC ->
case b1_adaM of { D# x3_adb0 ->
case divideC
@ (->) @ Double $s$fFractionalCat(->)a_shqs (lvl_siqR, boxD y_adaU)
of
{ D# d#_XfjM ->
case mulC
@ (->) @ Double $s$fNumCat(->)a_shlp (boxD x3_adb0, boxD d#_XfjM)
of
{ D# d#_XfjR ->
case lessThanOrEqual
@ (->)
@ Double
$s$fOrdCat(->)a_shnM
(case addC
@ (->)
@ Double
$s$fNumCat(->)a_shlp
(case mulC
@ (->) @ Double $s$fNumCat(->)a_shlp (boxD d#_XfjC, boxD d#_XfjC)
of
{ D# d#_XfjW ->
boxD d#_XfjW
},
case mulC
@ (->) @ Double $s$fNumCat(->)a_shlp (boxD d#_XfjR, boxD d#_XfjR)
of
{ D# d#_XfjW ->
boxD d#_XfjW
})
of
{ D# d#_XfjW ->
boxD d#_XfjW
},
lvl_siqX)
of {
False -> False;
True ->
exr
@ (->)
@ (R :* R)
@ ((R, R) -> Bool)
$fProductCat(->)
(($fYes1ka @ * @ (R, R), $fYes1ka @ * @ ((R, R) -> Bool))
cast(((%,%)
(Sym (R:Ok(->)[0]) <(Double, Double)>_N)
(Sym (R:Ok(->)[0]) <(Double, Double) -> Bool>_N))_R
:: ((Yes1 (Double, Double),
Yes1 ((Double, Double) -> Bool)) :: Constraint)
~R#
((Ok (->) (Double, Double),
Ok (->) ((Double, Double) -> Bool)) :: Constraint)))
(exl
@ (->)
@ (R :* R, (R, R) -> Bool)
@ (R, R)
$fProductCat(->)
(($fYes1ka @ * @ (R :* R, (R, R) -> Bool), $fYes1ka @ * @ (R, R))
cast(((%,%)
(Sym (R:Ok(->)[0]) <((Double, Double),
(Double, Double) -> Bool)>_N)
(Sym (R:Ok(->)[0]) <(Double, Double)>_N))_R
:: ((Yes1 ((Double, Double), (Double, Double) -> Bool),
Yes1 (Double, Double)) :: Constraint)
~R#
((Ok (->) ((Double, Double), (Double, Double) -> Bool),
Ok (->) (Double, Double)) :: Constraint)))
w_g_x_Xi)
wild_adaJ
}
}
}
}
}
}
}
}
}
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at src/ConCat/Plugin.hs:695:15 in concat-plugin-0.3.0.0-EuTio8PFqXo3nKN9zOJI1b:ConCat.PluginPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Progress 1/2
-- While building custom Setup.hs for package concat-graphics-0.1.0.0 using:
/Users/nasser/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_2.0.1.0_ghc-8.2.2 --builddir=.stack-work/dist/x86_64-osx/Cabal-2.0.1.0 build lib:concat-graphics test:graphics-examples --ghc-options " -ddump-hi -ddump-to-file -fdiagnostics-color=always"
Process exited with code: ExitFailure 1
🌙 [master*]$
🌙 [master*]$
🌙 [master*]$
🌙 [master*]$ stack build :misc-examples
concat-examples-0.3.0.0: test (suite: misc-examples)curry addC
Wrote add
dot -Gsize=10,10 -Tpdf out/add.dot -o out/add.pdf
/bin/sh: dot: command not found
misc-examples: user error (command "dot -Gsize=10,10 -Tpdf out/add.dot -o out/add.pdf" failed.)concat-examples-0.3.0.0: Test suite misc-examples failed
Test suite failure for package concat-examples-0.3.0.0
misc-examples: exited with: ExitFailure 1
Logs printed to console
I'm on macOS 10.13.2
Thanks
Restricting functor arguments
We're currently implementing a Category that will execute on the GPU via Accelerate.
A recurring issue is that in Accelerate, we can have arrays of numeric types (and tuples of them), but not nested arrays.
This goes counter to ConCat.Category's OkFunctor class that assumes that functors nest arbitarily.
We can work around this for OkFunctor by making Ok imply type inspection, but no such luck with Additive1. The best I could come up with is making Typeable a prerequisite for Additive, like this:
I tried making Typeable a prerquisite for additive1 instead, but this requires far more invasive and widespread changes, so I gave up eventually.
Add a "starter template" to the docs, for creating new categories
In https://gist.github.com/b88b24423732e2dc391569717059bf13 I have created a template, based on a dummy type, but which can serve as a quickstarter for building out new categories. Its features are:
- Every ConCat type class is given, except for
ArrayCat. - I show what the implementation looks like for
(->), to give a feel for what the arguments and return values from the classes are. - Not every class is needed to use
ccc, so users can comment out the classes they don't need until they do.
build error on ghc 8.2.2
Hey Conal, so i'm poking at seeing if i can quickly hack out the symmetric monoidal variant of concat using your stuff as a foundation and (among several things)
i hit the following error
src/ConCat/BuildDictionary.hs:123:38: error:
Variable not in scope: uniqSetToList :: VarSet -> [EvId]
|
123 | let givens = mkGivens loc (uniqSetToList evIds)
| ^^^^^^^^^^^^^
src/ConCat/BuildDictionary.hs:164:74: error:
Variable not in scope: uniqSetToList :: VarSet -> f1 Id
|
164 | pprTrace' "buildDictionary in-scope evidence" (ppr (WithType . Var <$> uniqSetToList scopedDicts)) $
| ^^^^^^^^^^^^^
src/ConCat/BuildDictionary.hs:206:31: error:
Variable not in scope: uniqSetToList :: VarSet -> f Var
|
206 | freeIdTys = varType <$> uniqSetToList freeIds
toCcc' rule not firing with GHC 8.2.2
Hm. With ghc 8.2.2, it looks like the "built-in rule" for toCcc' (doing most of the transformation work) never gets invoked. Investigating.
Should this auto diff example work?
I'm still getting accustomed to this library+plugin, and I think I'm confusing what happens at what phase. For instance, the following exhausts the rewrite ticks, so I assume there's a rewrite loop. Is it because deriv is trying to make the derivative's category (->)? I'm really not sure, this all seems quite magical, but in a good way!
x :: (Double, Double)
x = let f :: Double -> Double
f x = x ** 2 + 123
df :: Double -> (Double -> Double)
df x = deriv f x
in (f 10, df 10 10)Any chance I could get a hand with what I'm doing wrong?
Compiling to categories with dependent types
Haskell’s and GHC Core’s type systems impose severe limitations on the expressiveness of compiling to categories, including (but not only) the inability to express and verify the semantic correctness that lies just beneath the surface (homomorphic specifications and reasoning).
I have moved my category-based work over to Agda, where I’m able to address many more examples and verify their full correctness (not just properties). If anyone is interested in helping & playing, please let me know.
Simple, dependable recipe for client modules
For a concat client module to compile, GHC must be able to see some rewrite rules and some newtype constructors. I usually include the following import lines:
import qualified GHC.Generics -- needed to avoid coercion holes (sorry)
import ConCat.Rebox () -- rewrite rules
import ConCat.AltCat () -- rewrite rulesWe need the GHC.Generics import purely due to how the concat plugin translates coercions (into coerceC from the CoerceCat class), together with the following restriction:
You can unwrap a
newtypeusingcoerceonly if the corresponding constructor is in scope.
Without the import of GHC.Generics, the plugin will sometimes result in errors like the following:
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-apple-darwin):
ccc - couldn't build dictionary for
coerceC
@ (GD (Dual (-+>)))
@ ((:.:) (V 10) (Bump (V 4)) Double)
@ (V 10 (Bump (V 4) R)) :: CoerceCat
(GD (Dual (-+>)))
((:.:) (V 10) (Bump (V 4)) Double)
(V 10 (Bump (V 4) R)) =>
GD
(Dual (-+>))
((:.:) (V 10) (Bump (V 4)) Double)
(V 10 (Bump (V 4) R)):
coercion holes: [$dCoercible_aTpt
:: Coercible
(Vector Vector 10 (Bump (V 4) R))
((:.:) (V 10) (Bump (V 4)) Double)
[LclId, Str=DmdType]
$dCoercible_aTpt =
MkCoercible
@ *
@ (Vector Vector 10 (Bump (V 4) R))
@ ((:.:) (V 10) (Bump (V 4)) Double)
@~ (U(hole:{aTpu}, Vector Vector 10 (Bump (V 4) R), (:.:)
(V 10)
(Bump (V 4))
Double)_R
:: (Vector Vector 10 (Bump (V 4) R) :: *)
~R#
((:.:) (V 10) (Bump (V 4)) Double :: *)),
$dCoercible_aTpi
:: Coercible
((:.:) (V 10) (Bump (V 4)) Double)
(Vector Vector 10 (Bump (V 4) R))
[LclId, Str=DmdType]
$dCoercible_aTpi =
MkCoercible
@ *
@ ((:.:) (V 10) (Bump (V 4)) Double)
@ (Vector Vector 10 (Bump (V 4) R))
@~ (U(hole:{aTpj}, (:.:) (V 10) (Bump (V 4)) Double, Vector
Vector
10
(Bump (V 4) R))_R
:: ((:.:) (V 10) (Bump (V 4)) Double :: *)
~R#
(Vector Vector 10 (Bump (V 4) R) :: *))]
The failure here results from the (:.:) constructor (Comp1) not being in scope. A solution is to add "import qualified GHC.Generics".
This obscure issue keeps biting users. Maybe we could have a single import line for all concat users, like "import qualified ConCat", in addition to (probably unqualified) imports for operations actually used in client code.
I just added a ConCat module in plugin/:
{-# OPTIONS_GHC -Wall #-}
-- | For importing qualfied by ConCat clients. Enables some rewrite rules and
-- Coercible instances. Unfortunately, doing so leads to warnings of unused
-- imports in the client module. How to resolve (without -Wno-unused-imports)?
module ConCat (module GHC.Generics) where
import GHC.Generics -- needed to avoid coercion holes (sorry)
import ConCat.Rebox () -- rewrite rules
import ConCat.AltCat () -- rewrite rulesTried in a sample concat program (replacing those three imports). It works but generates a warning:
The qualified import of ‘ConCat’ is redundant
except perhaps to import instances from ‘ConCat’
To import instances alone, use: import ConCat()
If I add the "()", then the coercion hole error returns. Makes sense, though not what we want. Hm.
A possible solution might be to change the coerceC method definition in CoerceCat (->) and other CoerceCat instances.
Currently,
class CoerceCat k a b where
coerceC :: a `k` b
instance Coercible a b => CoerceCat (->) a b where
coerceC = coerceWhen synthesizing a use of coerceC, the plugin is already looking at a Core coercion between a and b, which it discards. It tries to synthesize a dictionary for CoerceCat k a b (for target category k), which sometimes leads to a coercion hole error. Could we instead use the coercion at hand? It's unclear to me how, since the general coerceC method doesn't involve Coercible. (Could it? Some of the instances are tricky due to coercion roles.)
Better yet, I'd love to redesign the handling of casts/coercions, eliminating CoerceCat altogether. My original intent was to transform Core cast expressions into combinations of existing categorical operations, using RepCat for the newtype axioms and (.) for the coercion transitivity.
Use of product categories is not compiling
When I try to do the following:
let prog :**: withLatency = ccc (uncurry (uncurry program))
putStrLn $ render prog
print $ curry (curry prog) 10 20 30I get this compiler error:
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-apple-darwin):
ccc - couldn't build dictionary for
. @ (t_apg7 :**: Any)
@ (Prod (->) Int Int)
@ Int
@ (Prod (->) Int Int, Int) :: (Category (t_apg7 :**: Any),
Ok3
(t_apg7 :**: Any)
(Prod (->) Int Int, Int)
(Prod (->) Int Int)
Int) =>
(:**:) t_apg7 Any (Prod (->) Int Int) Int
-> (:**:) t_apg7 Any (Prod (->) Int Int, Int) (Prod (->) Int Int)
-> (:**:) t_apg7 Any (Prod (->) Int Int, Int) Int:
free id types: [Category t_apg7, Category s_arqb[fuv:0]]
You can trigger the same error by editing the test in z3cat to use product categories.
Error in compiling graphic example.
Hi,
I am just checking out the code and following the instruction in README. But I am getting these errors for graphic examples:
➜ concat git:(master) stack build :graphics-examples
concat-graphics-0.1.0.0: build (lib + test)
Preprocessing library concat-graphics-0.1.0.0...
Preprocessing test suite 'graphics-examples' for concat-graphics-0.1.0.0...
[1 of 1] Compiling Main ( test/Examples.hs, .stack-work/dist/x86_64-osx/Cabal-1.24.2.0/build/graphics-examples/graphics-examples-tmp/Main.o )
/Volumes/First/Projects/concat/graphics/test/Examples.hs:176:35: error:
• Could not deduce (A.MonoidalPCat k) arising from a use of ‘A.&&&’
from the context: (A.ClosedCat k,
A.FloatingCat k R,
A.NumCat k R,
A.Ok k (R :* R),
A.Ok k (R -> R))
bound by the type signature for:
exampleC3' :: (A.ClosedCat k, A.FloatingCat k R, A.NumCat k R,
A.Ok k (R :* R), A.Ok k (R -> R)) =>
k R (R -> R)
at test/Examples.hs:(173,1)-(175,28)
Possible fix:
add (A.MonoidalPCat k) to the context of
the type signature for:
exampleC3' :: (A.ClosedCat k, A.FloatingCat k R, A.NumCat k R,
A.Ok k (R :* R), A.Ok k (R -> R)) =>
k R (R -> R)
• In the second argument of ‘(A..)’, namely ‘(A.exr A.&&& A.exl)’
In the first argument of ‘A.curry’, namely
‘(A.addC A.. (A.exr A.&&& A.exl))’
In the first argument of ‘(A..)’, namely
‘A.curry (A.addC A.. (A.exr A.&&& A.exl))’
Progress 1/2
-- While building custom Setup.hs for package concat-graphics-0.1.0.0 using:
/Users/anonym/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_1.24.2.0_ghc-8.0.2 --builddir=.stack-work/dist/x86_64-osx/Cabal-1.24.2.0 build lib:concat-graphics test:graphics-examples --ghc-options " -ddump-hi -ddump-to-file"
Process exited with code: ExitFailure 1
➜ concat git:(master) stack --version
Version 1.7.1, Git revision 681c800873816c022739ca7ed14755e85a579565 (5807 commits) x86_64 hpack-0.28.2
And for stack build :misc-examples --flag concat-examples:smt:
/Volumes/First/Projects/concat/examples/src/ConCat/SMT.hs:208:28: error:
• Could not deduce (MonoidalPCat k) arising from a use of ‘&&&’
from the context: (ConstCat k r, OrdCat k r, Ok k a)
bound by the type signature for:
andAbove :: (ConstCat k r, OrdCat k r, Ok k a) =>
k (a :* r) Bool -> r -> k (a :* r) Bool
at src/ConCat/SMT.hs:(206,1)-(207,59)
or from: ConCat.Category.Con (Ok' k (Prod k Bool Bool))
bound by a type expected by the context:
ConCat.Category.Con (Ok' k (Prod k Bool Bool)) => k (a :* r) Bool
at src/ConCat/SMT.hs:(208,20)-(211,26)
or from: ConCat.Category.Con (Ok' k (Prod k r r))
bound by a type expected by the context:
ConCat.Category.Con (Ok' k (Prod k r r)) => k (a :* r) Bool
at src/ConCat/SMT.hs:(208,20)-(210,23)
or from: ConCat.Category.Con (Ok' k (Prod k a r))
bound by a type expected by the context:
ConCat.Category.Con (Ok' k (Prod k a r)) => k (a :* r) Bool
at src/ConCat/SMT.hs:(208,20)-(209,23)
Possible fix:
add (MonoidalPCat k) to the context of
the type signature for:
andAbove :: (ConstCat k r, OrdCat k r, Ok k a) =>
k (a :* r) Bool -> r -> k (a :* r) Bool
• In the second argument of ‘(.)’, namely
‘(greaterThan . (exr &&& const lower) &&& f)’
In the first argument of ‘(<+)’, namely
‘andC . (greaterThan . (exr &&& const lower) &&& f)’
In the first argument of ‘(<+)’, namely
‘andC . (greaterThan . (exr &&& const lower) &&& f)
<+ okProd @k @a @r’
Progress 2/3
-- While building custom Setup.hs for package concat-examples-0.3.0.0 using:
/Users/watt/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_1.24.2.0_ghc-8.0.2 --builddir=.stack-work/dist/x86_64-osx/Cabal-1.24.2.0 build lib:concat-examples test:misc-examples --ghc-options " -ddump-hi -ddump-to-file"
Process exited with code: ExitFailure 1
I am on a MacOs High Sierra.
Thanks.
Split into separate repos?
As mentioned by @conal in #13 (comment), this could potentially be split into separate repos. I support this idea, for basically the same reasons as I made #91.
Basically, we use concat-classes and concat-examples in https://github.com/con-kitty/categorifier, but not concat-plugin. #91 solves the main issue, which is having concat-plugin in the graph. However, there are other changes we’d like to make to concat-classes/-examples (#99) that are easier if we don’t have to push them through the plugin as well.
I’m happy to make this happen if there is agreement about it. Also, I would like #91 to happen first, as it’s nicer history-wise to move things around in one repo than to move them across repos.
adding support for symmetric monoidal categories
i'm interested in making it easier for folks to experiment with fun stuff like linear logic and quantum physics, as we discussed last ICFP. My next 2-3 days of hacking / contribs is motivated by wanting to have that sort of vocab avaialble for EDSLs check in haskell. But even if i fail to hit that goal, would be handy to make it happen one way or another
Ideally i'd like to make sure i can bang that out for ghc 8.2 and such, but i'll see what i can do rocking 8.0.2 till you figure out the other issue with toCCC not getting optimized properly
How does one introduce new category classes to the ConCat plugin?
Do you have any documentation on how we introduce new category classes to the plugin, and how we identify which Haskell functions should be represented in the abstraction by methods of those classes?
Introduction of ConstCat instance unexpectedly changing result of toCcc
I'm playing with a toy example of defining my own categorical instances in order to get a feel for using the plugin, and I'm running into unexpected behavior. I have a data type to record the categorical expressions generated, and I'm trying to transform a simple function to that. Note that my data type has a constructor that isn't covered by any of the categorical type classes, so I'm using unCcc with that.
With the code as is, this all works fine. For example, the function:
f :: () -> (Bool, Bool)
f () = let x = prim 0.0
y = prim 0.0
in (x,y)... is transformed into:
Comp (Const ?) (Comp (Dup) (Par (Prim) (Prim)))
... which is correct. The unexpected part, is that when I uncomment this ConstCat instance and re-run stack run, the output changes to:
Comp (Dup) (Par (Const ?) (Const ?))
... which is not what I expect -- the Prim arrows have disappeared.
I'd be grateful to hear any suggestions about what might be happening and how I might fix this.
Here's the output I see with the plugin debug flags set on the erroneous case:
concat-example-0.1.0.0: unregistering (local file changes: src/MyLib.hs)
concat-example> configure (lib + exe)
Configuring concat-example-0.1.0.0...
concat-example> build (lib + exe)
Preprocessing library for concat-example-0.1.0.0..
Building library for concat-example-0.1.0.0..
[2 of 2] Compiling MyLib
Preprocessing executable 'concat-example-exe' for concat-example-0.1.0.0..
Building executable 'concat-example-exe' for concat-example-0.1.0.0..
[1 of 2] Compiling Main [MyLib changed]
go ccc C:
f
:: () -> (Bool, Bool)
Doing top unfold
toCcc'
f
-->
toCcc'
@ C
@ ()
@ (Bool, Bool)
(\ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ })
go ccc C:
\ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ }
:: () -> (Bool, Bool)
Doing lam Case nullary
toCcc'
\ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ }
-->
toCcc' @ C @ () @ (Bool, Bool) (\ (ds_d3uJ :: ()) -> lvl_s7JJ)
go ccc C:
\ _ [Occ=Dead] -> lvl_s7JJ
:: () -> (Bool, Bool)
Couldn't build dictionary for
const @ C @ (Bool, Bool) @ () :: (ConstCat C (Bool, Bool),
Ok C ()) =>
(Bool, Bool) -> C () (ConstObj C (Bool, Bool)):
no bindings
Doing lam unfold
toCcc'
\ _ [Occ=Dead] -> lvl_s7JJ
-->
toCcc'
@ C @ () @ (Bool, Bool) (\ _ [Occ=Dead] -> (lvl_s7JG, lvl_s7JI))
go ccc C:
\ _ [Occ=Dead] -> (lvl_s7JG, lvl_s7JI)
:: () -> (Bool, Bool)
Couldn't build dictionary for
const @ C @ (Bool, Bool) @ () :: (ConstCat C (Bool, Bool),
Ok C ()) =>
(Bool, Bool) -> C () (ConstObj C (Bool, Bool)):
no bindings
Doing lam Pair
toCcc'
\ _ [Occ=Dead] -> (lvl_s7JG, lvl_s7JI)
-->
&&&
@ C
@ ()
@ Bool
@ Bool
($fProductCatC, $fMonoidalPCatC)
(($fYes1ka @ * @ (), $fYes1ka @ * @ Bool, $fYes1ka @ * @ Bool)
`cast` (((%,,%)
(Sym (R:OkC[0]) <()>_N)
(Sym (R:OkC[0]) <Bool>_N)
(Sym (R:OkC[0]) <Bool>_N))_R
:: (Yes1 (), Yes1 Bool, Yes1 Bool)
~R# (Ok C (), Ok C Bool, Ok C Bool)))
(toCcc' @ C @ () @ Bool (\ _ [Occ=Dead] -> lvl_s7JG))
(toCcc' @ C @ () @ Bool (\ _ [Occ=Dead] -> lvl_s7JI))
go ccc C:
\ _ [Occ=Dead] -> lvl_s7JG
:: () -> Bool
Doing lam mkConst'
toCcc'
\ _ [Occ=Dead] -> lvl_s7JG
-->
const
@ C
@ Bool
@ ()
$fConstCatCBool
(($fYes1ka @ * @ ())
`cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ()))
lvl_s7JG
go ccc C:
\ _ [Occ=Dead] -> lvl_s7JI
:: () -> Bool
Doing lam mkConst'
toCcc'
\ _ [Occ=Dead] -> lvl_s7JI
-->
const
@ C
@ Bool
@ ()
$fConstCatCBool
(($fYes1ka @ * @ ())
`cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ()))
lvl_s7JI
ccc final:
[lvl_s7JG :: Bool
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]
lvl_s7JG = prim (D# 0.0##),
lvl_s7JI :: Bool
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]
lvl_s7JI = prim (D# 0.0##),
lvl_s7JJ :: (Bool, Bool)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
lvl_s7JJ = (lvl_s7JG, lvl_s7JI),
f :: () -> (Bool, Bool)
[LclIdX,
Arity=1,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
f = \ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ },
$trModule_s4GG :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s4GG = "main"#,
$trModule_s4GH :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s4GH = TrNameS $trModule_s4GG,
$trModule_s4GI :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s4GI = "Main"#,
$trModule_s4GJ :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s4GJ = TrNameS $trModule_s4GI,
$trModule :: Module
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
$trModule = Module $trModule_s4GH $trModule_s4GJ,
main_s6ni :: String
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 190 0}]
main_s6ni
= $fShowC_$cshow
@ ()
@ (Bool, Bool)
(reveal
@ C
@ ()
@ (Bool, Bool)
(&&&
@ C
@ ()
@ Bool
@ Bool
($fProductCatC, $fMonoidalPCatC)
(($fYes1ka @ * @ (), $fYes1ka @ * @ Bool, $fYes1ka @ * @ Bool)
`cast` (((%,,%)
(Sym (R:OkC[0]) <()>_N)
(Sym (R:OkC[0]) <Bool>_N)
(Sym (R:OkC[0]) <Bool>_N))_R
:: (Yes1 (), Yes1 Bool, Yes1 Bool)
~R# (Ok C (), Ok C Bool, Ok C Bool)))
(const
@ C
@ Bool
@ ()
$fConstCatCBool
(($fYes1ka @ * @ ())
`cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ()))
lvl_s7JG)
(const
@ C
@ Bool
@ ()
$fConstCatCBool
(($fYes1ka @ * @ ())
`cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ()))
lvl_s7JI))),
main :: IO ()
[LclIdX,
Arity=1,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 40 60}]
main = hPutStr' stdout main_s6ni True,
main_s7JA :: State# RealWorld -> (# State# RealWorld, () #)
[LclId,
Arity=1,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 60}]
main_s7JA = runMainIO1 @ () main,
main :: IO ()
[LclIdX,
Arity=1,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
main
= main_s7JA
`cast` (Sym (N:IO[0] <()>_R)
:: (State# RealWorld -> (# State# RealWorld, () #)) ~R# IO ())]
P.S. Thanks for sharing this wonderful work!
support GHC 9
I started implementing this, and was progressing nicely with fairly minor changes (the GHC API module names have changed, a few functions now take an extra arg, ...), but I ran into an issue that might be more significant.
In https://gitlab.haskell.org/ghc/ghc/-/commit/0de03cd78729dc58a846c64b645e71057ec5d24e, RuleFun was changed from taking DynFlags to a more restricted RuleOpts, so ConCat.Satisfy.Plugin.satisfy no longer has access to the full DynFlags structure.
I think the only place that concat seriously uses the DynFlags is in ConCat.Simplify, but I'm not sure how to work around the lack of it there.
Inefficient categorical IR?
This is not so much a bug report but a technical question:
In your papers, an expression such as x + (x * y) would be encoded as add ￮ (exl △ mul). However, your compiler extension uses dup instead. This seems to lead to inefficiencies.
I am therefore wondering: what is the reason for the difference between the categorical operators in your papers and the implementation? Is it due to the way GHC works? Or does it solve some other issues? Could the above inefficiencies be avoided by using the more "rudimentary" categorical operators that you use in your papers?
Many thanks in advance for your time!
CtWanted and GHC 8.2.2 in ConCat.BuildDictionary
Compile-time warning:
/Users/conal/Haskell/concat/satisfy/src/ConCat/BuildDictionary.hs:140:24: warning: [-Wmissing-fields]
• Fields of ‘CtWanted’ not initialised: ctev_nosh
• In the second argument of ‘($)’, namely
‘CtWanted
{ctev_pred = predTy, ctev_dest = EvVarDest evar, ctev_loc = loc}’
In the expression:
mkNonCanonical
$ CtWanted
{ctev_pred = predTy, ctev_dest = EvVarDest evar, ctev_loc = loc}
In an equation for ‘nonC’:
nonC
= mkNonCanonical
$ CtWanted
{ctev_pred = predTy, ctev_dest = EvVarDest evar, ctev_loc = loc}
|
140 | CtWanted { ctev_pred = predTy
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Try a simple example anyway:
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64-apple-darwin):
/Users/conal/Haskell/concat/examples/src/ConCat/BuildDictionary.hs:(140,24)-(142,50): Missing field in record construction ctev_nosh
I don't know why GHC is mis-reporting the file name for ConCat.BuildDictionary
synthesizing hardware via functional programming
@conal I enjoy reading you paper, finding new concepts; a lot of new concepts in fact; I would say most of it is new to me 😄
If I understand correctly, your project and paper addressing an issue of HW synthesis from functional description.
I have 20ish years of RTL design experience with slowly growing frustration about how tedious is this cruft. Verilog is VERY low level language, it is gives you job security but takes your life for it.
I have tried multiple approaches of generating Verilog in different languages (TCL, Perl, JavaScript) and based on different description forms including computation digraphs and ASTs.
Lately I am learning functional programming (in format of JavaScript) with plans to apply some of it to hardware description techniques. Admit, that I don't have formal education on functional programming or deep lambda-calculus knowledge. So my learning process a bit slow.
I guess what I am trying to say is: I would be glad to share / work together on the subject if you find it appealing / interesting or / and it meets you research agenda.
Orphans in hidden packages
buildDictionary filters out orphans from hidden modules:
-- Remove hidden modules from dep_orphans
orphans <- filterM (moduleIsOkay env0) (moduleName <$> dep_orphs (mg_deps guts))That means if A imports B, B imports C, and C is in a hidden package when compiling A, then I don't think the orphan instances in C will be found by buildDictionary, even though C is transitively imported by A.
I think GHC does consider such orphan instances when resolving type class constraints. I wonder if what buildDictionary does is a deliberate design choice?
Unboxed types and operations
Reboxing (described in section 10.1 of Compiling to categories) has been consistently challenging and it feels like a place where I'm working at odds with GHC. An alternative is to go with the flow, aiming at unboxed primitive types and operations. I think doing so would require introducing levity polymorphism to the category classes. My previous attempts ran into some GHC bugs that might have been fixed in GHC 8.2.
Dictionary construction failures and GHC 8.2.2
After this commit getting past issue #41 (with ctev_nosh = WOnly), I get a little further. The next error message I get is from the plugin itself, reporting that dictionary construction failed:
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64-apple-darwin):
ccc - couldn't build dictionary for
exr @ (->) @ Double @ Double :: (ProductCat (->),
Ok2 (->) Double Double) =>
(->):
no bindings
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at src/ConCat/Plugin.hs:1132:23 in concat-plugin-0.3.0.0-EuTio8PFqXo3nKN9zOJI1b:ConCat.Plugin
I tested by running stack build :misc-examples with only the following example enabled in test/Examples.hs:
, runSynCirc "add" $ toCcc $ (+) @RReboxing failures
The reboxing scheme described in section 10.1 of Compiling to categories sometimes fails. Collect examples here, and mull over improved schemes.
Update build instructions (possible Nix build motivation?)
Cloned the repo and tried to run stack build :misc-examples as instructed in the README. Greeted with:
Configuring z3-4.1.0...
Cabal-simple_mPHDZzAJ_1.24.2.0_ghc-8.0.2: Missing dependency on a foreign
library:
* Missing (or bad) header file: z3.h
* Missing C library: z3
This problem can usually be solved by installing the system package that
provides this library (you may need the "-dev" version). If the library is
already installed but in a non-standard location then you can use the flags
--extra-include-dirs= and --extra-lib-dirs= to specify where it is.
If the header file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
which doesn't surprise me given the SMT example. It'd be fair to say this is a non-issue, but perhaps we can entertain the possible of a Nix-build? cc @jwiegley
buildDictionary isn't finding instances in the module being compiled
Example:
data Foo = Foo Double
negateFoo :: Unop Foo
negateFoo (Foo x) = Foo (negate x)
instance HasRep Foo where
type Rep Foo = R
abst x = Foo x
repr (Foo x) = x
foo1 :: Foo -> Foo :* (Foo -> Foo)
foo1 = andDerF negateFooCoproducts?
Hi,
I have a question. What is the status of coproduct support? Do they work? If they do, how to use them? Are there any working examples (couldn't find one)? If they don't, what should be done to make them work, or are there any alternatives? (I've seen a comment with "instance HasRep (a :+ b)" in Rep.hs implementing coproduct in terms of product, dunno if that's a good lead)
I tried to add this:
, runSyn $ toCcc $ \x -> Left x :: Either Int Int
to the examples, which results in an "oops: toCcc' called", even though there is an instance CoproductCat Syn.
Here is the last message of the trace
go ccc Syn:
Left @ Int @ Int
:: Int -> Either Int Int
Couldn't build dictionary for
reprC @ (->) @ (Either Int Int) @ (Rep (Either Int Int)) :: RepCat
(->)
(Either Int Int)
(Rep (Either Int Int)) =>
Either Int Int
-> Rep (Either Int Int):
free id types: [HasRep (Either Int Int)]
Doing top Unhandled
when I changed "Left" to "A.inl" (from AltCat), the example worked.
Investigating, I've found a rule
"toCcc Prelude Left" toCcc Left = toCcc inl
in AltCat, which would seem to solve this problem, however it's between #if 0, #endif. Why?
Goal: I would like to pass expressions involving Either (in standard Haskell, so Left, Right etc.) into toCcc, and then provide an implementation of coproducts in the category I'm working on (actually that last part I already did).
I would also like to translate ADTs into sums. For example, I have a category Kat implementing coproducts and a simple "instance r ~ Rep a => RepCat Kat a r". When I try the following:
data E = L | R
instance HasRep E where
type Rep E = Either () ()
repr L = Left ()
repr R = Right ()
abst (Left ()) = L
abst (Right ()) = R
{-# INLINE repr #-}
{-# INLINE abst #-}
then running toCcc on
f :: Int -> E
f _ = L
results in an infinite compilation loop. This message shows up often:
Couldn't build dictionary for
const @ Kat @ E @ (Either () ()) :: (ConstCat Kat E,
Ok Kat (Either () ())) =>
E -> Kat (Either () ()) (ConstObj Kat E):
no bindings
seems like the plugin expects me to provide a ConstCat instance for E which, if I understand correctly, I shouldn't need to provide. Occurrences of E should be translated into Either () ()s, right? Maybe some rule is not fired for some reason.
When I change the HasRep instance to
instance HasRep E where
type Rep E = Bool
repr L = False
repr R = True
abst False = L
abst True = R
{-# INLINE repr #-}
{-# INLINE abst #-}
it works. So it seems that the plugin doesn't like Eithers?
GHC panic when compiling examples
I ran "stack build :misc-examples" and got:
Preprocessing test suite 'misc-examples' for concat-examples-0.3.0.0...
[1 of 1] Compiling Main ( test\Examples.hs, .stack-work\dist\ca59d0ab\build\misc-examples\misc-examples-tmp\Main.o )
ghc.EXE: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-mingw32):
Simplifier ticks exhausted
When trying RuleFired cat equal
To increase the limit, use -fsimpl-tick-factor=N (default 100)
If you need to do this, let GHC HQ know, and what factor you needed
To see detailed counts use -ddump-simpl-stats
Total ticks: 51001
Not sure if it's an actual GHC bug, or something to do with the plugin?
Instance resolution fails for instances defined in module being compiled
It appears that instance resolution fails for instances defined in module being compiled. To investigate.
New application: Haskell to SQL (f="SELECT * FROM table;" length<$>f="SELECT COUNT(*) FROM table;")
Let's say we have an SQL database containing a comments table.
In our Haskell code, we have a DB function fetchComments :: m [Comment] which, behind the scenes, runs an SQL query and returns a list of comments. In the code that consumes this DB function, sometimes we would like to just get the number of comments, so we would write length <$> fetchComments.
So, I've been thinking: is it possible to use the library in this repo to have fetchComments generate, by default, an SQL string that looks something like "SELECT * FROM comments;", whereas, if length is applied to the return value of fetchComments in the code, the resulting SQL string would be "SELECT COUNT(*) FROM comments;"?
So, in other words, rather than having the SQL server send all the comments (possibly thousands, or millions) over the write, the length transformation -- that would otherwise be applied in application code -- is applied by the SQL server, since length <$> fetchComments is translated into a different SQL query than just fetchComments alone.
Metaprogramming/escaping ccc?
Is it possible to manipulate the ccc expression using normal functions as I'm trying to do below?
For simple things it seems it can work because you can inline them, something like the foldCat I've given below won't work because foldr1 won't be inlined and then ccc does it's work and replaces the arrows.
{-# INLINE foldCat #-}
foldCat :: (Ok3 k a b (Prod k a b), ConstCat k a, ClosedCat k) => [a] -> Prod k a b `k` b -> b `k` b
foldCat xs f = foldr1 (.) $ map (flip applyConst f) xs
{-# INLINE applyConst #-}
applyConst :: (Ok4 k a b c (Prod k a b), ConstCat k a, ClosedCat k) => a -> Prod k a b `k` c -> b `k` c
applyConst a f = f . (const a &&& id)
main :: IO ()
main = print $ render (ccc program)
where program xs = foldCat xs addC
Documentation on Running Simple Program using AD
I'm trying to play with the AD facilities, so decided to start with a minimal example.
import ConCat.ADFun
d :: (Double -> a) -> Double -> a
d f x = derF f x 1
main = do
print $ d id 0 -- should be 1
print $ d (\x -> x*(d (x*) 2)) 1 -- should be 2Placing this as nest.hs in the top-level concat directory and running stack ghc nest.hs generates nest but
$ ./nest
nest: Oops: toCcc' called
I tried to turn on options etc, see below, to get this migrated to compile-time, but must not have tickled the right ones. This is a beautiful system, and I'd like to play with it using the nice exported API without delving down into the internals. A few tiny examples of how to do this would really help.
{-# OPTIONS_GHC -fplugin=ConCat.Plugin #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -O2 #-}
import ConCat.ADFun
-- Define a restricted form of the d operator.
d :: (Double -> a) -> Double -> a
d f x = derF f x 1
{-# INLINE d #-}
unnested :: Double
unnested = d id 0 -- should be 1
{-# INLINE unnested #-}
nested :: Double
nested = d (\x -> x*(d (x*) 2)) 1 -- should be 2
{-# INLINE nested #-}
main :: IO ()
main = do
putStr "unnested, should be 1: "
print unnested
putStr "nested, should be 2: "
print nestedImproved handling of GHC Core coercions
A consistent pain point has been GHC Core coercions. As with reboxing, I'm struggling to undo the effects of GHC optimizations. I've repeatedly tried and failed to find a simple and complete scheme for turning GHC Core coercions into a simple form that composes and generalizes to other categories. I'd like to target the simple class of representation changers in ConCat.Category:
class RepCat k a r | a -> r where
reprC :: a `k` r
abstC :: r `k` aThe tricky part is that newtype conversions become GHC Core coercions, which then get optimized together and need unweaving. I've coped by adding another class:
class CoerceCat k a b where coerceC :: a `k` bHaving both RepCat and CoerceCat feels clunky to me.
[Question] Compiling to EVM bytecodes?
Hi,
Love the technique in general, I am just wondering, has anyone happen to think how much work would it need to compile some haskell code to EVM bytecodes using ConCat?
Cheers,
haddock building failure
stack build --haddock produces the following error message:
concat-classes-0.3.0.0: configure (lib)
concat-classes-0.3.0.0: build (lib)
concat-classes-0.3.0.0: haddock
Log files have been written to: /Users/cshao/concat/.stack-work/logs/
Progress: 1/4
-- While building package concat-classes-0.3.0.0 using:
/Users/cshao/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_1.24.2.0_ghc-8.0.2 --builddir=.stack-work/dist/x86_64-osx/Cabal-1.24.2.0 haddock --html --html-location=../$pkg-$version/ --haddock-option=--hyperlinked-source
Process exited with code: ExitFailure 1
Logs have been written to: /Users/cshao/concat/.stack-work/logs/concat-classes-0.3.0.0.log
Configuring concat-classes-0.3.0.0...
Preprocessing library concat-classes-0.3.0.0...
Running Haddock for concat-classes-0.3.0.0...
Preprocessing library concat-classes-0.3.0.0...
Haddock coverage:
18% ( 10 / 56) in 'ConCat.Misc'
Missing documentation for:
:* (src/ConCat/Misc.hs:42)
:+ (src/ConCat/Misc.hs:43)
:=> (src/ConCat/Misc.hs:44)
absurdF (src/ConCat/Misc.hs:63)
PrimBasics (src/ConCat/Misc.hs:85)
Evalable (src/ConCat/Misc.hs:89)
Unop (src/ConCat/Misc.hs:95)
Binop (src/ConCat/Misc.hs:96)
Ternop (src/ConCat/Misc.hs:97)
Yes0 (src/ConCat/Misc.hs:113)
(src/ConCat/Misc.hs:114)
Yes1 (src/ConCat/Misc.hs:116)
(src/ConCat/Misc.hs:117)
Yes2 (src/ConCat/Misc.hs:119)
(src/ConCat/Misc.hs:120)
inNew (src/ConCat/Misc.hs:122)
inNew2 (src/ConCat/Misc.hs:126)
exNew (src/ConCat/Misc.hs:132)
exNew2 (src/ConCat/Misc.hs:136)
xor (src/ConCat/Misc.hs:146)
Parity (src/ConCat/Misc.hs:150)
(src/ConCat/Misc.hs:152)
(src/ConCat/Misc.hs:157)
boolToInt (src/ConCat/Misc.hs:161)
&& (src/ConCat/Misc.hs:171)
(src/ConCat/Misc.hs:172)
&+& (src/ConCat/Misc.hs:178)
(src/ConCat/Misc.hs:179)
Flip (src/ConCat/Misc.hs:181)
(src/ConCat/Misc.hs:182)
FoldrC (src/ConCat/Misc.hs:190)
MapC (src/ConCat/Misc.hs:194)
AndC (src/ConCat/Misc.hs:202)
AllC (src/ConCat/Misc.hs:203)
++ (src/ConCat/Misc.hs:217)
CrossWith (src/ConCat/Misc.hs:221)
AllC2 (src/ConCat/Misc.hs:229)
bottom (src/ConCat/Misc.hs:251)
typeR (src/ConCat/Misc.hs:256)
R (src/ConCat/Misc.hs:259)
sqr (src/ConCat/Misc.hs:261)
magSqr (src/ConCat/Misc.hs:264)
transpose (src/ConCat/Misc.hs:267)
inTranspose (src/ConCat/Misc.hs:270)
underF (src/ConCat/Misc.hs:282)
overF (src/ConCat/Misc.hs:287)
50% ( 2 / 4) in 'ConCat.Rep'
Missing documentation for:
inAbst (src/ConCat/Rep.hs:228)
inAbst2 (src/ConCat/Rep.hs:233)
10% ( 21 /220) in 'ConCat.Category'
Missing documentation for:
U2 (src/ConCat/Category.hs:86)
(src/ConCat/Category.hs:92)
Monoid2 (src/ConCat/Category.hs:101)
HasCon (src/ConCat/Category.hs:107)
Sat (src/ConCat/Category.hs:112)
(src/ConCat/Category.hs:114)
(src/ConCat/Category.hs:119)
|- (src/ConCat/Category.hs:125)
(src/ConCat/Category.hs:127)
(src/ConCat/Category.hs:132)
(src/ConCat/Category.hs:137)
(src/ConCat/Category.hs:141)
&& (src/ConCat/Category.hs:159)
OpCon (src/ConCat/Category.hs:161)
Yes1' (src/ConCat/Category.hs:170)
Ok' (src/ConCat/Category.hs:172)
OpSat (src/ConCat/Category.hs:174)
inSat (src/ConCat/Category.hs:176)
inOpL (src/ConCat/Category.hs:179)
inOpR (src/ConCat/Category.hs:182)
inOpL' (src/ConCat/Category.hs:185)
inOpR' (src/ConCat/Category.hs:196)
inOpLR (src/ConCat/Category.hs:202)
(src/ConCat/Category.hs:207)
(src/ConCat/Category.hs:211)
C1 (src/ConCat/Category.hs:225)
C2 (src/ConCat/Category.hs:226)
C3 (src/ConCat/Category.hs:227)
C4 (src/ConCat/Category.hs:228)
C5 (src/ConCat/Category.hs:229)
C6 (src/ConCat/Category.hs:230)
Ok2 (src/ConCat/Category.hs:240)
Ok3 (src/ConCat/Category.hs:241)
Ok4 (src/ConCat/Category.hs:242)
Ok5 (src/ConCat/Category.hs:243)
Ok6 (src/ConCat/Category.hs:244)
Oks (src/ConCat/Category.hs:246)
Category (src/ConCat/Category.hs:255)
(src/ConCat/Category.hs:281)
(src/ConCat/Category.hs:287)
(src/ConCat/Category.hs:293)
(src/ConCat/Category.hs:297)
(src/ConCat/Category.hs:301)
(src/ConCat/Category.hs:305)
(src/ConCat/Category.hs:309)
Prod (src/ConCat/Category.hs:320)
OkProd (src/ConCat/Category.hs:324)
okProd (src/ConCat/Category.hs:326)
(src/ConCat/Category.hs:411)
(src/ConCat/Category.hs:424)
(src/ConCat/Category.hs:429)
transposeP (src/ConCat/Category.hs:476)
(src/ConCat/Category.hs:490)
Coprod (src/ConCat/Category.hs:514)
okCoprod (src/ConCat/Category.hs:516)
(src/ConCat/Category.hs:574)
(src/ConCat/Category.hs:585)
(src/ConCat/Category.hs:596)
(src/ConCat/Category.hs:601)
transposeS (src/ConCat/Category.hs:647)
DistribCat (src/ConCat/Category.hs:665)
(src/ConCat/Category.hs:696)
(src/ConCat/Category.hs:702)
(src/ConCat/Category.hs:706)
okExp (src/ConCat/Category.hs:734)
Exp (src/ConCat/Category.hs:744)
ClosedCat (src/ConCat/Category.hs:747)
(src/ConCat/Category.hs:763)
applyK (src/ConCat/Category.hs:769)
curryK (src/ConCat/Category.hs:770)
uncurryK (src/ConCat/Category.hs:771)
(src/ConCat/Category.hs:785)
(src/ConCat/Category.hs:805)
Unit (src/ConCat/Category.hs:818)
OkUnit (src/ConCat/Category.hs:820)
TerminalCat (src/ConCat/Category.hs:822)
(src/ConCat/Category.hs:826)
(src/ConCat/Category.hs:830)
(src/ConCat/Category.hs:834)
(src/ConCat/Category.hs:837)
lunit (src/ConCat/Category.hs:841)
runit (src/ConCat/Category.hs:844)
constFun (src/ConCat/Category.hs:860)
constFun2 (src/ConCat/Category.hs:871)
unitFun (src/ConCat/Category.hs:876)
unUnitFun (src/ConCat/Category.hs:880)
ConstObj (src/ConCat/Category.hs:891)
ConstCat (src/ConCat/Category.hs:907)
repConst (src/ConCat/Category.hs:937)
pairConst (src/ConCat/Category.hs:946)
(src/ConCat/Category.hs:965)
(src/ConCat/Category.hs:984)
(src/ConCat/Category.hs:988)
(src/ConCat/Category.hs:992)
DelayCat (src/ConCat/Category.hs:1003)
(src/ConCat/Category.hs:1006)
LoopCat (src/ConCat/Category.hs:1010)
(src/ConCat/Category.hs:1013)
&+& (src/ConCat/Category.hs:1037)
(src/ConCat/Category.hs:1038)
Constrained (src/ConCat/Category.hs:1048)
(src/ConCat/Category.hs:1050)
(src/ConCat/Category.hs:1056)
(src/ConCat/Category.hs:1061)
(src/ConCat/Category.hs:1067)
(src/ConCat/Category.hs:1073)
BoolOf (src/ConCat/Category.hs:1090)
BoolCat (src/ConCat/Category.hs:1092)
(src/ConCat/Category.hs:1103)
(src/ConCat/Category.hs:1111)
(src/ConCat/Category.hs:1119)
(src/ConCat/Category.hs:1125)
okTT (src/ConCat/Category.hs:1135)
EqCat (src/ConCat/Category.hs:1138)
(src/ConCat/Category.hs:1144)
(src/ConCat/Category.hs:1149)
(src/ConCat/Category.hs:1154)
(src/ConCat/Category.hs:1158)
OrdCat (src/ConCat/Category.hs:1164)
(src/ConCat/Category.hs:1172)
(src/ConCat/Category.hs:1179)
(src/ConCat/Category.hs:1186)
(src/ConCat/Category.hs:1192)
EnumCat (src/ConCat/Category.hs:1202)
(src/ConCat/Category.hs:1209)
(src/ConCat/Category.hs:1213)
(src/ConCat/Category.hs:1217)
NumCat (src/ConCat/Category.hs:1223)
(src/ConCat/Category.hs:1230)
(src/ConCat/Category.hs:1238)
(src/ConCat/Category.hs:1246)
(src/ConCat/Category.hs:1253)
IntegralCat (src/ConCat/Category.hs:1265)
divModC (src/ConCat/Category.hs:1270)
(src/ConCat/Category.hs:1274)
(src/ConCat/Category.hs:1279)
(src/ConCat/Category.hs:1284)
(src/ConCat/Category.hs:1288)
FractionalCat (src/ConCat/Category.hs:1294)
(src/ConCat/Category.hs:1303)
(src/ConCat/Category.hs:1308)
(src/ConCat/Category.hs:1313)
(src/ConCat/Category.hs:1317)
FloatingCat (src/ConCat/Category.hs:1323)
(src/ConCat/Category.hs:1326)
(src/ConCat/Category.hs:1332)
(src/ConCat/Category.hs:1338)
(src/ConCat/Category.hs:1343)
RealFracCat (src/ConCat/Category.hs:1351)
(src/ConCat/Category.hs:1355)
(src/ConCat/Category.hs:1361)
(src/ConCat/Category.hs:1367)
(src/ConCat/Category.hs:1372)
FromIntegralCat (src/ConCat/Category.hs:1382)
(src/ConCat/Category.hs:1387)
(src/ConCat/Category.hs:1391)
(src/ConCat/Category.hs:1395)
(src/ConCat/Category.hs:1398)
BottomCat (src/ConCat/Category.hs:1403)
bottomRep (src/ConCat/Category.hs:1406)
(src/ConCat/Category.hs:1412)
(src/ConCat/Category.hs:1415)
(src/ConCat/Category.hs:1417)
(src/ConCat/Category.hs:1420)
IfT (src/ConCat/Category.hs:1424)
IfCat (src/ConCat/Category.hs:1426)
(src/ConCat/Category.hs:1429)
(src/ConCat/Category.hs:143
src/ConCat/AltCat.hs:156:3: error:
parse error on input ‘{- | C.curry without the eager inlining -}’
3)
(src/ConCat/Category.hs:1437)
(src/ConCat/Category.hs:1440)
unitIf (src/ConCat/Category.hs:1444)
okIf (src/ConCat/Category.hs:1447)
prodIf (src/ConCat/Category.hs:1450)
funIf (src/ConCat/Category.hs:1474)
repIf (src/ConCat/Category.hs:1494)
UnknownCat (src/ConCat/Category.hs:1510)
(src/ConCat/Category.hs:1513)
(src/ConCat/Category.hs:1516)
(src/ConCat/Category.hs:1519)
RepCat (src/ConCat/Category.hs:1523)
(src/ConCat/Category.hs:1527)
(src/ConCat/Category.hs:1531)
(src/ConCat/Category.hs:1535)
TransitiveCon (src/ConCat/Category.hs:1541)
(src/ConCat/Category.hs:1544)
CoerceCat (src/ConCat/Category.hs:1550)
(src/ConCat/Category.hs:1555)
(src/ConCat/Category.hs:1558)
(src/ConCat/Category.hs:1561)
Arr (src/ConCat/Category.hs:1611)
ArrayCat (src/ConCat/Category.hs:1613)
(src/ConCat/Category.hs:1621)
arrayFun (src/ConCat/Category.hs:1627)
arrAtFun (src/ConCat/Category.hs:1631)
(src/ConCat/Category.hs:1637)
(src/ConCat/Category.hs:1642)
AmbCat (src/ConCat/Category.hs:1677)
(src/ConCat/Category.hs:1679)
(src/ConCat/Category.hs:1683)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.