Skip to content

Instantly share code, notes, and snippets.

@ssaavedra

ssaavedra/operator.hs

Created November 7, 2016 13:30
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 ssaavedra/b5d2e5987fc12f485e9cb84c99740ec6 to your computer and use it in GitHub Desktop.
Save ssaavedra/b5d2e5987fc12f485e9cb84c99740ec6 to your computer and use it in GitHub Desktop.
Download ZIP
Haskell and higher-order polymorphism. Intuitionstic logic and type theory.
Raw
operator.hs
{-# LANGUAGE RankNTypes #-}
module Operator
where
(***) f g (x1, x2) = (f x1, g x2)
f :: [a] -> [a]
f = snd . splitAt 1
type GType a = ([a], [a])
f' :: [a] -> GType a
f' = splitAt 1
g :: [a] -> Int
g = length
-- Naïve type:
-- (???) :: (t -> t1) -> (t, t) -> (t1, t1)
type FType c a = c
myCoercion :: (f a -> c) -> (f a -> FType c a)
myCoercion a = a
(???) :: (forall a. f a -> g a) -> (f a, f b) -> (g a, g b)
(???) f (x1, x2) = (f *** f) (x1, x2)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment