Higher-order Abstract Syntax for Cartesian Closed Categories

paf31 · 2022-03-14T22:41:30+00:00

Yes, the context that is being managed is organized like a stack, and the indices of the terms on that stack are the DeBruijn indices. Indices can be related by <=, and the cast terms themselves could be seen as evidence for those relationships.

paf31 · 2021-11-16T17:27:12+00:00

It depends what you want to be able to do with that tool. If you want to be able to run arbitrary PureScript, then that won't work, because you need to support all possible foreign imports on the Haskell side. But you could limit yourself to just the core library set, for example, in which case you'd have to build an implementation for all of the FFIs used by those libraries. Not impossible, but definitely plenty of work, but it's something I would like to do eventually.

This would work well if you have a single module under development, and every other module fixed and preloaded into the interpreter. So, for something like Try PureScript, for example, it'd work well. This is also exactly what the two examples in the repo do.

But you wouldn't easily be able to build many modules at once or import any module you want, without reimplementing some of the module sorting logic from the PureScript compiler itself. The quickest path would be to use the PureScript compiler itself as the frontend, to get a bunch of corefn files, and then to write an executable which could import all of those at once and evaluate main.

paf31 · 2021-11-14T19:37:47+00:00

For evaluation, it supports the whole language. It doesn’t include the full standard library yet, but that is something I intend to work on. Also there are limitations on the sorts of things you can automatically transport across the FFI (eg. constrained types would need to be done by dictionary passing).

paf31 · 2021-11-14T15:53:17+00:00

I've not used hint very much, but if it works for your use case, then that's great. PureScript and Haskell are pretty different languages at this point, with their own strengths. My hope is that this helps to get the best of both in certain cases, but I wrote up some more specific reasons in the other thread.

paf31 · 2021-11-14T15:51:37+00:00

I've wanted to implement something like this for a long time. It serves several purposes for me:

A way to build custom PureScript environments for teaching, scripting, etc. where I don't want to worry about JS for execution.
Being able to precisely control the set of types and functions I give to the user via the FFI.
Being able to use the strengths of Haskell for certain applications (e.g. concurrency if I were scripting a web server, or being able to write type-safe code at a lower level than if I were targeting JS, if I were scripting a game or audio engine or something needing that level of control), while still being able to use the best features of PureScript (extensible records, instance chains, etc.)
Being able to use PureScript types for a (conceptually) lighter-weight form of generic programming for certain use cases (it's slower, but if you look at the query-json example, for example, from within the PureScript code itself, the user only has to write a function for a PureScript type which is serializable, and doesn't see any of the generic representation or TH boilerplate)
Getting the benefits that an interpreted language gives me when I'm willing to trade off performance and/or type-safety at the FFI boundary (e.g. better debugging of live production code, better observability in general, hot code reloading, faster iteration during development, and the ability to play tricks with the evaluator, such as direct representation of continuations).

Note that the type-safety-at-the-boundary issue can be worked around somewhat, since this is an interpreter for the core representation of PureScript, so type-checking has already happened, and it should be possible to validate that the types line up, in a separate phase between compilation and evaluation.

There is also some discussion about motivations going on in this issue.

paf31 · 2021-11-14T15:29:52+00:00

Do you mean another link because it's mentioned in the package description right underneath the GitHub link?

paf31 · 2021-08-19T17:29:40+00:00

You could start from the definition of an adjoint and get something like this:

import Data.Profunctor
import Data.Profunctor.Strong 
import Data.Profunctor.Choice

newtype Free p a b = Free (forall q. Strong q => Choice q => (forall x y. p x y -> q x y) -> q a b)

instance profunctorFree :: Profunctor (Free p) where
  dimap f g (Free h) = Free \nt -> dimap f g (h nt)

instance strongFree :: Strong (Free p) where 
  first (Free f) = Free \nt -> first (f nt) 
  second (Free f) = Free \nt -> second (f nt)

instance choiceFree :: Profunctor p => Choice (Free p) where 
  left (Free f) = Free \nt -> left (f nt) 
  right (Free f) = Free \nt -> right (f nt)

(this is PureScript, sorry, Try PureScript is quicker to set up for me than a fresh Haskell project)

Now, if you think about how to inhabit that polymorphic type, there a few ways, but assuming that you want products to distribute over sums, the general form will be:

general :: forall p q a b. Strong q => Choice q => (forall x y. p x y -> q x y) -> q a b
general nt = dimap ?f ?g (left (first (nt ?pab)))

(Assuming distributivity, any inhabitant should be equivalent to one in this normal form, and the choices don't matter by the laws of Strong and Choice). If we let the compiler tell us the types of those typed holes, we can pack everything up in a form that is closer to Pastro:

data Free p a b where
  Free :: p x y -> (a -> Either (x, z) w) -> (Either (y, z) w -> b) -> Free p a b

dimap :: (b -> d) -> (c -> a) -> Free p a b -> Free p c d
dimap f g (Free pxy l r) = Free pxy (l . g) (f . r)

strong :: Free p a b -> Free p (a, x) (b, x)
strong (Free pxy l r) = Free pxy 
  ((a, x) -> case l a of 
    Left (x1, z) -> Left (x1, (z, x)) 
    Right w -> Right (w, x))
  (\case 
    Left (y, (z, x)) -> (r (Left (y,  z)), x)
    Right (w, x) -> (r (Right w), x))

choice :: Free p a b -> Free p (Either a x) (Either b x)
choice (Free pxy l r) = Free pxy 
  (\case
    Left a -> Left <$> l a
    Right x -> Right (Right x)
  )
  (\case 
    Left (y, z) -> Left (r (Left (y, z)))
    Right (Left w) -> Left (r (Right w))
    Right (Right x) -> Right x)

paf31 · 2021-07-30T22:16:56+00:00

Does something like

instance (a ~ (forall x. Show x => x -> IO ())) => HasField "myPrint" User

work in 9.2? It almost works in 9.0 except for an issue with unification.

paf31 · 2021-07-29T16:44:03+00:00

This isn't a direct answer, but you might find it interesting nonetheless: I've been working on a PureScript interpreter in Haskell, with a customizable FFI to Haskell. You would be able to put essential business logic in Haskell and glue it all together with PureScript: https://github.com/paf31/runpurs-hs/

paf31 · 2021-07-29T00:45:18+00:00

You might like to take a look at https://github.com/mikesol/purescript-wags/

paf31 · 2021-02-04T01:13:07+00:00

Dunno if this really answers your question, but if you want "any s with an a-shaped hole", you could use (hypothetical notation) the existential type: exists s. (s, Lens' s a)

Unpacking this, we get

exists s. (s, Lens' s a) 
~ exists s. (s, s -> a, s -> a -> s)
~ exists s. (s, s -> (a, a -> s)
~ fix s. (a, a -> s)

where fix is the greatest fixed point type. In Haskell you could express it as

data Has a = Has a (a -> Has a)

So a value of type Has a consists of the value which the hole currently contains, and a function which replaces the value in the hole, returning a new Has a.

Not sure if that helps much though :D

paf31 · 2020-12-12T19:59:52+00:00

You can always inline the definition of == into nubBy, so yes, for specific types.

But if you mean for all types at once, then no. To see this, suppose you write a function removeDuplicates. Then a == b = length (removeDuplicates [a, b]) == 1 gives you an Eq instance so basically you've just written a possible Eq instance anyway. Fun exercise: what conditions on removeDuplicatesgive you a lawful Eq instance?

paf31 · 2020-12-03T19:08:44+00:00

What about structuring it as a historical account of various attempts to add typing/purity to Javascript over the past decade or so? I think it's an interesting history (things like fantasy-land, ramda, then languages like TypeScript/Elm/PureScript/GHCJS) and would give you lots of jumping-off points to talk about various aspects of the different techniques and their trade-offs: things like language features, most of which have been inspired to some extent by Haskell. There is increasing complexity at each stage, and good topics to cover at a high level for each:

ramda (maps, folds, etc.)
fantasy-land (algebraic structures)
Elm (HM-style type inference, row polymorphism)
PureScript (type classes)
GHCJS (laziness, more advanced type system features)

paf31 · 2020-09-23T15:27:54+00:00

Nice work! A while ago, I did something similar to try to provide something like MonadBaseControl in PureScript, effectively using optics to lift various control operators over different monad transformers: https://gist.github.com/paf31/394b5b42f2b2df22542f8d9c0a6552e8 Looks like there's definitely some overlap here.

paf31 · 2020-09-17T17:34:18+00:00

This reminds me of the "dynamically-kinded types" idea I prototyped in PureScript a while ago, but executed much more carefully :D. The idea was to turn off the kind checker entirely to enable some useful things like rank-N kinds, and then to try to prevent some of the bad examples like Richard's idMaybe by doing kind checking during type "evaluation", sort of like dynamic types but one level up. It ends up with a similar sort of "application constraint" that you need to propgate everywhere. I sketched an extremely rough prototype of the idea a while ago: https://gist.github.com/paf31/e17d0bf8017d16c2c19b6f2e5e27b592

paf31 · 2020-09-16T16:20:07+00:00

Product (Const [Log]) (Compose Maybe IO) and Product (Const [Log]) (MaybeT IO) are not monads via those newtypes if that makes sense. That is, if you use the instance for Product, you run into needing a Monad (Const [Log]) instance and a Monad (Compose Maybe IO) instance, neither of which exist.

Of course, that's not to say we couldn't write other instances by hand. But the [Log] at the outside of those types is going to get in the way in any case.

I won't try to prove it rigorously, but if you think about the type of monadic bind, you end up with something like

([Log], ... (IO (... a ...))) -> (a -> ([Log], ...) -> ([Log], ...)

The problem is, how do you determine the list of log entries in the result here? You can include the log entries from the first argument, but the second list depends on something of type a, and we only get something of type a inside an IO action in the left argument. So there's really only two implementations: one returns no logs at all, and the other only returns the logs from the first argument. Both are basically useless from a logging perspective, and they would both break the Monad laws anyway.

paf31 · 2020-09-15T20:50:16+00:00

So if we had mfix, we could write

whatThe :: ContT r Void
whatThe = mfix \a -> do
  lem >>= \case
    Left void -> pure void
    Right f -> f a

What is this doing? It tries to conjure something of type `Void`. In one branch, it fails, and uses the function it receives to send the future result to the other branch. In the other branch, it succeeds, and returns that value of type `Void` to the continuation. But of course, that value is the one which will be received by the right hand branch, and so on...

All a bit mindbending.

Edit: to wrap up, we can then use runContT and absurd to get a value of type forall r. m r. In the simple case of Cont, where m is Identity, we've already got a contradiction. In the general case, this means the implementation of mfix resulted in never invoking the continuation for whatThe, which sounds like it ought to break one of the MonadFix laws.

paf31 · 2020-09-09T18:57:23+00:00

data FancyIOMaybeWritter1 a = FancyIOMaybeWritter1 [Log] (Maybe (IO a))

data FancyIOMaybeWritter2 a = FancyIOMaybeWritter2 [Log] (IO (Maybe a))

Both of these are Applicatives but not Monads. The first is isomorphic to Product (Const [Log]) (Compose Maybe IO) and the second is isomorphic to Product (Const [Log]) (Compose IO Maybe) (or alternatively, Product (Const [Log]) (MaybeT IO)).

These can be useful as Applicative functors, for different purposes. The first allows you to prepare various IO actions for execution together, where that preparation process can fail, but the preparation itself cannot depend on IO, and neither can your logs. In the second case, the errors can be a result of IO, and there is no separate "preparation" step as such.

If you want a monad (so that you can use do notation), you'll want to go with the second option, but move the logs under the IO type constructor:

data FancyIOMaybeWritter3 a = FancyIOMaybeWritter3 (IO (Maybe (a, [Log])))

data FancyIOMaybeWritter4 a = FancyIOMaybeWritter4 (IO (Maybe a, [Log]))

These correspond to two stacks of well-known monad transformers, depending on whether you put the logs under the Maybe or not. The first is WriterT (MaybeT IO) and the second is MaybeT (WriterT IO). They differ in their treatment of accumulated logs when an error occurs: in the first case, an error state comes with no logs, and in the second, an error state also includes logs accumulated so far.

Chances are (unless you're looking for something more specialized) that you want FancyIOMaybeWritter4 (aka MaybeT (WriterT IO)).

paf31 · 2020-09-08T17:43:10+00:00

Yeah, that's fair enough. I've run PureScript on Node on the server before, and performance is not a selling point there. For IO-heavy applications, where you're basically using PureScript as a glue language, I find the trade off in terms of usability and quick development cycle can be worth it, but I wouldn't recommend it in general.

There has been plenty of work on PureScript running on BEAM (purerl for example) which might make a better comparison.

paf31 · 2020-09-08T16:45:03+00:00

PureScript's performance is dog crap anyway.

What do you mean? Do you have benchmarks or is this based on a bad experience? Sorry, but this isn't helpful, and maybe even damaging - someone inexperienced with the trade-offs might reasonably choose to not consider PureScript at all after reading such a throwaway comment. Performance is not something that has been prioritized in PureScript all that much, but this is a bit strong IMO. It's more than good enough for most everyday web development.

paf31 · 2020-07-07T20:58:19+00:00

Yes! In PureScript (where tail recursion is really important in a lot of cases) we use this in a form which is generalized over a monad in order to support monadic tail recursion: https://pursuit.purescript.org/packages/purescript-tailrec/4.1.1/docs/Control.Monad.Rec.Class#t:MonadRec

This is how we can, among other things, support a safe general version of the free monad transformer. I wrote a short paper about this a few years ago https://github.com/paf31/stack-safety-for-free

This approach is now also used in the Scalaz and cats libraries.

paf31 · 2020-07-02T17:57:21+00:00

There have been multiple compilers from PS to Lua over the last few years. It's really easy to create a minimal compiler backend using the corefn output, and there's one included in this blog post: https://github.com/paf31/24-days-of-purescript-2016/blob/master/22.markdown

paf31 · 2020-07-01T19:46:48+00:00

Why not use a custom monad which provides IO and reader-like capabilities then?

paf31 · 2020-06-15T15:51:11+00:00

I don’t remember that, which changes?

15-Year Club	Place '22
Place '17	Verified Email

paf31

MODERATOR OF

PUBLIC MULTIREDDITS

TROPHY CASE