Skip to content

Instantly share code, notes, and snippets.

@jmatsushita
Created July 2, 2020 12:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jmatsushita/c544c34971cecfd61528fa06c996460b to your computer and use it in GitHub Desktop.
Save jmatsushita/c544c34971cecfd61528fa06c996460b to your computer and use it in GitHub Desktop.
Problem type checking with natural transformation in record type
module Main where
import Prelude
import Effect (Effect)
import Data.Foldable (fold)
import TryPureScript (h1, text, render)
data Nat m n = Nat (m ~> n)
data NatR m n = NatR { nat :: (m ~> n) }
morphS :: forall m n. Monad m => Monad n => (m ~> n) -> m Unit -> n Unit
morphS t fm = t fm
-- useR :: forall m n. Monad m => Monad n => NatR m n -> m Unit -> n Unit
-- useR (NatR { nat }) x = morphS nat x -- Error!
-- Error: Could not match type a4 with a1
-- a4 rigid type variable bound at line 17, column 34-54...
-- Stays at line 17 even if I move the code around.
-- Actually it's also the same location in my local code base... Wat?
useR' :: forall m n. Monad m => Monad n => NatR m n -> m Unit -> n Unit
useR' (NatR h) x = morphS h.nat x -- Works
useR'' :: forall m n. Monad m => Monad n => NatR m n -> m Unit -> n Unit
useR'' (NatR h) = morphS h.nat -- Pointfree also works
main :: Effect Unit
main =
render $ fold
[ h1 (text "Try natural transformation in records!")
]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment