Using VSCode Neovim with a separate config

Zachary Churchill — Wed, 24 Aug 2022 03:54:00 +0000

I'm primarily a neovim user, but occasionally, for pairing with my coworkers remotely, I'll use vscode.

using this option

allows you to set an init folder different from the default, as I've done here.

One problem that many neovim users may run into is that if you use neovim's native plugins feature (even through a package manager), any plugins that are broken or obsoleted by vscode are still in your rtp. Here's how you fix that:

The --clean flag removes the plugins directory from your runtime path before neovim starts, you can still opt into plugins as I've done here

vim.opt.rtp:append(os.getenv('HOME') .. '/.config/nvim-code')
vim.opt.rtp:append(os.getenv('HOME') .. '/.local/share/nvim/site/pack/packer/start/tabular/')

require('plugins.unload')
require('settings')
require('keybindings')

I hope this helps you stay comfy when working with coworkers :)
no more ctrl+w closing my editor for me.

Trasa tutorial pt. 1: Type safe web routing with trasa

Zachary Churchill — Fri, 17 May 2019 02:24:13 +0000

`trasa`: type safe HTTP routing and dispatch in Haskell

Hello, World!

Dependencies

  build-depends: base ^>=4.12.0.0
    , trasa
    , trasa-server
    , quantification
    , bytestring
    , wai
    , wai-extra
    , warp

For the sake of brevity, I'll be putting all of the code in the same cabal package. These are the minimal dependencies for getting a web server up and running. trasa can leverage wai and warp to handle the webserver/webapp component.

quantification is maybe the only library you might not recognize here. It's used internally by trasa, you'll want it in order to get better error messages and eventually to annotate some type signatures.

Extensions

{-# language DataKinds #-}
{-# language GADTs #-}
{-# language KindSignatures #-}
{-# language OverloadedStrings #-}
{-# language ScopedTypeVariables #-}

trasa uses GADTs and TypeFamilies extensively in its internals in an attempt to strike a balance between type level magic like seen in servant and value level haskell. This tutorial only assumes familiarity with GADTs, which we'll use to define a Route type.

Imports

import Data.ByteString.Lazy (ByteString)
import Data.Functor.Identity
import Data.Kind (Type)
import Network.Wai (Application)
import Network.Wai.Handler.Warp (run)
import Network.Wai.Middleware.RequestLogger (logStdoutDev)
import Trasa.Core
import Trasa.Server
import qualified Data.ByteString.Lazy as B
import qualified Trasa.Method as Method

Our Route type

-- Our route data type. We define this ourselves.
data Route :: [Type] -> [Param] -> Bodiedness -> Type -> Type where
  HelloWorld :: Route 
    '[] -- ^ the route does not capture any part of the path
    '[] -- ^ the route does not capture any queries
    'Bodyless -- ^ the route does not have a request body
    ByteString -- ^ the response body will be `ByteString`

trasa is polymorphic in the 'route' type. This means we can trivially deviate from a type that looks like this, such as annotating Route with documentation.

Our HelloWorld constructor represents a route that does not decode any path pieces and does not have any query parameters. For the response body, we must define a BodyCodec for the request and response type we chose. ByteString has the most trivial definition of a body codec:

bodyText :: BodyCodec ByteString
bodyText = BodyCodec 
  (pure "text/html; charset=utf-8") -- ^ NonEmpty list of the HTTP media type names.
  id -- ^ encode @ByteString -> ByteString@
  Right -- ^ decode @ByteString -> Either Text ByteString@

(The utf-8 encoded Text would be more correct than ByteString here. If you want, you may define a bodyText :: BodyCodec Text as an exercise)

Providing metadata for our Route type

-- | metadata about our routes: value level functions and data for constructing
--   and decoding paths
meta :: Route captures queries request response -> MetaCodec captures queries request response
meta route = case route of
  HelloWorld -> Meta 
    (match "hello" ./ end) -- ^ match "/hello"
    qend -- ^ no query parameters
    bodyless -- ^ no request body
    (resp (one bodyText)) -- ^ response body is one BodyCodec: our bodyText function above
    Method.get -- ^ http method: GET

Since the Route GADT doesn't actually carry information about our route (like its HTTP method or the textual representation of its path), we define a function where we pattern match on the data constructor and supply this information using functions from trasa

Route handling

-- | this function defines how we handle routes with our web server:
--   what actions we perform based on the route and its captures & queries
routes
  :: forall captures queries request response.
     Route captures queries request response -- ^ our route GADT, polymorphic over its type variables
  -> Rec Identity captures -- ^ an extensible record of the captures for this route
  -> Rec Parameter queries -- ^ an extensible record of the captures for this route
  -> RequestBody Identity request -- ^ the request body
  -> TrasaT IO response -- ^ our response
routes route captures queries reqBody = case route of
  HelloWorld -> go helloWorld
  where
  -- | this helper function uses the `handler` function to unwrap the `Arguments` type family.
  go :: Arguments captures queries request (TrasaT IO response) -> TrasaT IO response
  go f = handler captures queries reqBody f

helloWorld :: TrasaT IO ByteString
helloWorld = pure "Hello, World!"

This function will be used by the webserver to determine what actions to take based on what Route data constructor is matched. We are presented with:

our Route data constructor
an extensible record of each value captured in the path
an extensible record of each query parameter
the request body

The go helper function uses handler to supply these to the function it's passed. The handler function and Arguments type family help keep everything fully polymorphic.

helloWorld is the function that takes all of the arguments from the captures and queries (in this case none) and resolves that to the response body type. The TrasaT IO part of the type allows us to do nice error handling and IO, we will ignore boilerplate.

The webserver

-- | We define a list of all the routes for our server, 
--   this is the only place where the type checker won't help us
allRoutes :: [Constructed Route]
allRoutes = [Constructed HelloWorld]

-- | Boilerplate. This creates the data structure used to do routing
router :: Router Route
router = routerWith (mapMeta captureDecoding captureDecoding id id . meta) allRoutes

-- | `wai` application
application :: Application
application = serveWith
  (metaCodecToMetaServer . meta) -- ^ boilerplate: this just marshals some types
  routes -- ^ routes function defined above
  router -- ^ router function defined above

main :: IO ()
main = run 8080 (logStdoutDev application)

Now run cabal run, xdg-open http://localhost:8080/hello and you should be greeted with "Hello, World!"

Captures and queries

Ok, ok, cool. Now we can do some basic routing, but here's the best feature of trasa in my opinion: captures and queries. Say instead of "Hello, world!" we want something slightly more complicated. Say we want "$0, $1!". Let's modify the type of the HelloWorld constructor a bit:

data Route :: [Type] -> [Param] -> Bodiedness -> Type -> Type where
  HelloWorld :: Route 
    '[ByteString] -- ^ now the path captures the first piece as a ByeString
    '[('Optional ByteString)] -- ^ there is an optional query parameter, decoded as a ByteString
    'Bodyless -- ^ the route does not have a request body
    ByteString -- ^ the response body will be `ByteString`

Now we've got type errors to fix.

src/Main.hs:(37,17)-(42,14): error:
    • Couldn't match type ‘'[]’ with ‘'[ByteString]’
      Expected type: MetaCodec captures queries request response
        Actual type: Meta
                       CaptureCodec
                       CaptureCodec
                       (Many BodyCodec)
                       (Many BodyCodec)
                       '[]
                       '[]
                       'Bodyless
                       ByteString
...
   |
37 |   HelloWorld -> Meta
   |                 ^^^^^...
src/Main.hs:54:20-29: error:
    • Couldn't match type ‘TrasaT IO ByteString’
                     with ‘ByteString -> Maybe ByteString -> TrasaT IO ByteString’
      Expected type: Arguments
                       captures queries request (TrasaT IO response)
        Actual type: TrasaT IO ByteString
    • In the first argument of ‘go’, namely ‘helloWorld’
      In the expression: go helloWorld
      In a case alternative: HelloWorld -> go helloWorld
   |
54 |   HelloWorld -> go helloWorld

We get a slightly opaque type error in our meta function, but the error from our routes function is slightly more illuminating. To solve this first error, let's look at the type from three functions in trasa:

match :: Text -> Path cpf caps -> Path cpf caps
capture :: cpf cap -> Path cpf caps -> Path cpf (cap ': caps)
end :: Path cpf '[]

and the HelloWorld metadata from our meta function:

  HelloWorld -> Meta 
    (match "hello" ./ end) -- ^ match "/hello"
    qend -- ^ no query parameters
    bodyless -- ^ no request body
    (resp (one bodyText)) -- ^ response body is one BodyCodec: our bodyText function above
    Method.get -- ^ http method: GET

The type error is telling us that the path has the type Path cpf '[] because match will not extend end, but what the type checker is inferring is Path cpf '[ByteString]. The story is similar for the query parameter. Lets solve this:

-- add `text` as a dependency
import qualified Data.Text.Encoding as TE
import qualified Data.ByteString.Lazy as B
import qualified Trasa.Method as Method
-- define a CaptureCodec for ByteString: encoding and decoding to and from text
bytestring :: CaptureCodec ByteString
bytestring = CaptureCodec (TE.decodeUtf8 . B.toStrict) (Just . B.fromStrict . TE.encodeUtf8)
-- I'm still not going to change this to Text for now. We'll fix this later

Change helloWorld to take its path captures and query parameters as arguments:

helloWorld :: ByteString -> Maybe ByteString -> TrasaT IO ByteString
helloWorld a (Just b) = pure $ a <> ", " <> b <> "!"
helloWorld a Nothing = pure a

Use the helper functions from trasa and the bytestring capture codec to add metadata about how to decode the HelloWorld path:

  HelloWorld -> Meta 
    (capture bytestring ./ end) -- ^ capture "/$0"
    (optional "b" bytestring .& qend) -- ^ optionally capture "?b=$1"
    bodyless -- ^ no request body
    (resp (one bodyText)) -- ^ response body is one BodyCodec: our bodyText function above
    Method.get -- ^ http method: GET

Rerun, and voilà!

Code: https://github.com/goolord/trasa-tutorial/tree/master/trasa-ex-pt1

DEV Community: Zachary Churchill