Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
See if this still fails on GHC 8.2
type Cat k = k -> k -> Type
data T = D | I
type family
Interp (a :: T) :: Type where
Interp I = Int
Interp D = Double
data Fn :: (T, T) -> Type where
Exp :: Fn '(D, D)
Sqrt :: Fn '(D, D)
Mod :: Int -> Fn '(I, I)
Round :: Fn '(D, I)
(:.:) :: Fn '(b, c) -> Fn '(a, b) -> Fn '(a, c)
eval :: Fn '(a, b) -> Arr Interp0 (->) a b
eval Exp = Arr exp
eval Sqrt = Arr sqrt
eval Round = Arr round
eval (Mod m) = Arr (`mod` m)
eval (f:.:g) = eval f . eval g
newtype Arr :: (a ~> Type) -> Cat Type -> Cat a where
Arr :: (cat (ty_fam ^ a) (ty_fam ^ b)) -> Arr ty_fam cat a b
newtype Arr' (cat :: Cat k) a b where
Arr' :: (cat a b) -> Arr' cat a b
deriving Category
-- instance forall k_ab1l k_ab1m (cat_ab1n :: Cat k_ab1m).
-- Category cat_ab1n =>
-- Category (Arr' cat_ab1n) where
-- id
-- = coerce
-- (Control.Category.id :: cat_aaWR a_a6y3 a_a6y3) ::
-- forall (a_a6y3 :: k_Xb0s). Main.Arr' cat_aaWR a_a6y3 a_a6y3
-- (.)
-- = coerce
-- ((.) ::
-- cat_aaWR b_a6y4 c_a6y5
-- -> cat_aaWR a_a6y6 b_a6y4 -> cat_aaWR a_a6y6 c_a6y5) ::
-- forall (b_a6y4 :: k_Xb0s) (c_a6y5 :: k_Xb0s) (a_a6y6 :: k_Xb0s).
-- Arr' cat_aaWR b_a6y4 c_a6y5
-- -> Arr' cat_aaWR a_a6y6 b_a6y4
-- -> Arr' cat_aaWR a_a6y6 c_a6y5
instance Category cat => Category (Arr ty_fun cat) where
id = Arr id
Arr f . Arr g = Arr (f . g)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
data Interp0 :: T ~> Type
type family
(f :: a ~> b) ^ (x :: a) :: b where
Interp0 ^ a = Interp a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment