If it’s easy to set up and maintain something similar to head.hackage then that sounds like an interesting way to do it.
1 Like
There’s other ways to do it, but if you want to do it the head.hackage way, the repo is here: https://gitlab.haskell.org/ghc/head.hackage
and here’s the older, shell script simpler way GitHub - hvr/head.hackage: This is not the Git repo you're looking for...
Here’s cabal’s basic docs on the three types of repositories it can accept (although you can teach microcabal about any sort you desire!) 4.1. Configuration — Cabal 3.17.0.0 User's Guide
a no-index is arguably the easiest of all to setup, and may suffice for your purposes in fact.
1 Like
Using something like head.hackage is quite neat. But it is a burden on anyone who wants to use MicroHs. Furthermore, it’s cements the impression that MicroHs is the ugly step-child who is not welcome to play in the beautiful GHC garden called Hackage.
6 Likes
Is there any strategy on how to deal with libraries that make use of TemplateHaskellQuotes/QuasiQuotes, since TH is not supported?
IsString (or rather OverloadedStrings) is not an alternative, because it can’t encode failure. In those cases, we don’t really need the full power of TH. The function I want to run at compile time doesn’t strictly require IO (or at least it’s hidden):
encodeWith :: TextEncoding -> String -> Either EncodingException PosixString
I know there have been ideas floating around regarding a language extension that’s a subset of TH. I don’t know if any of that would appeal to you. I could also imagine a variant of OverloadedStrings where logic regarding string literals is hardcoded in the compiler instead of deferring it to class instances at runtime. That might allow some encoding/decoding logic and emitting warnings/errors. But I don’t have a very concrete proposal.
4 Likes
I think it should be doable to support compiling libraries that define Quasiquoters, derive Lift instances or use TemplateHaskellQuotes without committing to running TH splices, and that would let you compile lots more code without CPP (eg, you can’t run TH splices while boostrapping GHC, but you can compile these things). You might even be able to do something hacky like define the TH AST types to be the empty type or something and then all of these become trivial. (Of course then you wouldn’t be able to use the quasiquoters, lift instances, etc)
It would also be good if we had a more lightweight alternative to TH. There is a huge design space here that would be well worth exploring.
3 Likes
I agree that specifically the ability to have compile-time parsed and checked strings and other literals, without otherwise being “TH” would be extremely useful – there were definitely a few GHC proposals on this, but none quite seemed to be elegant enough to find widespread support.
5 Likes
I think statically verified strings is totally doable with MicroHs with a little extra compiler work.
I’ll give it some thought, since it’s a fun problem.
5 Likes
I’ll implement statically verified strings tomorrow if I have a few hours hacking time. It shouldn’t be hard. Famous last words…
8 Likes
Would an approach like this work with MicroHs?
type FromType :: forall {k}. k -> Type -> Constraint
class FromType t a where
type KnownType t a :: Constraint
fromType :: (KnownType t a) => proxy t -> a
Obviously it’s not nearly as powerful as a full blown QQ, but maybe you could turn a Symbol into an OsString with it.
I was looking into this idea for completely unrelated reasons, so I wouldn’t be surprised if it’s not actually applicable. But if people are interested, I made a little library for it here: literally: Convert type literals into values.
1 Like
That would not work with MicroHs. There are no type families. I’m going to do something simpler. There’ll be a function compileTime :: a->a that will tell the compiler to run the computation at compile time. It’s a useful thing to have.
5 Likes
There’ll be a function
compileTime :: a->athat will tell the compiler to run the computation at compile time. It’s a useful thing to have.
It’s highly useful — but also ill-defined as a function, no? 
Unless it includes evaluation of expression with variables, e.g.
foo :: Int → Int
foo x = compileTime (head [x * x])
would be evaluated to
foo :: Int → Int
foo x = compileTime (x * x)
at compile time.
Unless it includes evaluation of expression with variables
MicroHs uses (extended) SKI combinators under the hood, so evaluation of expressions with variables shouldn’t be a big problem. The only thing I’m worried about is how to know how much to inline.
What is a “statically verified string”?
Incidentally @TeofilC is leading an effort to partition the interface to Template Haskell into parts, so the clients who rely only on simple, stable parts (like quasiquoters) can rely on a library whose API is stable. You might find that design worht a look.
@TeofilC is there one place where your plan is summarised?
5 Likes
My HEW talk is probably the most up-to-date version of the plan in its entirety: https://www.youtube.com/watch?v=TCvDq6ScaDg
For the design of these smaller libraries, see: Splitting out stable subsets from `template-haskell` (`template-haskell-lift` and `template-haskell-quasiquote`) by TeofilC · Pull Request #696 · ghc-proposals/ghc-proposals · GitHub
They are almost ready to be released, and I should have a blog post up soon announcing them
With these smaller libraries, I think it would be easier to for instance add a new constructor to Quasiquoter that only allows checking a string literal, and letting that be implemented by both GHC and MicroHS
Sure — but my point is that the expression compileTime (head [x * x]) is not a closed expression in lambda calculus, because it has a free variable x. As far as I understand, only closed expressions can be represented using SKI combinators.
Put differently, the question is: What’s the semantics of compileTime when the argument has free variables?
To a first approximation, the semantics is compileTime = id, but that’s too coarse — clearly the function does something useful beyond id . Evaluating the argument to WHNF at compile time sounds like a viable semantics to me, but this requires evaluation of open terms.
1 Like
It would be nice to deal with open terms, but I’m going to do something simpler. For compilrTime e to be well defined, the free variables of the e must only be top level definitions.
2 Likes
For
compileTime eto be well defined, the free variables of theemust only be top level definitions.
Fair enough — that’s well-defined and does something useful.
Unrelatedly, I’m beginning to think that the ability to evaluate open terms goes a long way towards compiler-checked proofs. After all, proving that a function has some property forall xs involves evaluation of that function with xs being a variable. In order to conclude such a proof, we eventually need to perform a check along the lines of “Is \xs → xs is the identity function?”. We can’t do this check at runtime because that would break referential transparency, but at compile time, we can use the loophole that we can make the program fail compilation if the check does not succeed — referential transparency is preserved for all programs that do compile, we just compile fewer programs.
Sometimes, I wonder about an alternate history of Haskell where Haskell compilers are also proof assistants for Haskell by tradition. (De-emphasizing Curry-Howards, but keeping the Haskell syntax.)
1 Like
If you’re interested in open terms, you may want to take a look at Beluga – a proof assistant designed to handle binding and open terms specifically well: Beluga
In the QualifiedLiterals GHC proposal (now closed and split into smaller ones) there was some talk about being able to define functions that would be run at compile-time. This would be less general than the compileTime solution; each module would have its own function for a concrete type (and I guess it wouldn’t need evaluation of open terms?)
I take it back. There’s some tricky points in getting it working.
1 Like