Created
September 19, 2018 10:12
-
-
Save phadej/707d620cdfb315f30f51e8deeacffcde to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE TypeOperators #-} | |
-- For the "Another take" | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE TypeSynonymInstances #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# OPTIONS_GHC -Wall #-} | |
import Data.Type.Nat | |
import Data.Proxy | |
import qualified Data.Vec.Lazy as V | |
------------------------------------------------------------------------------- | |
-- From the paper: | |
------------------------------------------------------------------------------- | |
type s :-> t = forall i. s i -> t i | |
class IFunctor f where | |
imap :: (s :-> t) -> f s :-> f t | |
data Path :: ((k,k) -> *) -> (k,k) -> * where | |
Stop :: Path g '(i, i) | |
(:-:) :: g '(i, j) -> Path g '(j, k) -> Path g '(i, k) | |
instance IFunctor Path where | |
imap _ Stop = Stop | |
imap f (r :-: rs) = f r :-: imap f rs | |
class IFunctor m => IMonad (m :: (k -> *) -> k -> *) where | |
iskip :: p :-> m p | |
iextend :: (p :-> m q) -> (m p :-> m q) | |
------------------------------------------------------------------------------- | |
-- IMonad Path | |
------------------------------------------------------------------------------- | |
pathAppend :: Path g '(i, j) -> Path g '(j, k) -> Path g '(i, k) | |
pathAppend Stop q = q | |
pathAppend (r :-: rs) q = r :-: pathAppend rs q | |
instance IMonad Path where | |
iskip _x = undefined -- x :-: Stop -- cannot write, as GHC is silly :/ | |
iextend _ Stop = Stop | |
iextend f (r :-: rs) = pathAppend (f r) (iextend f rs) | |
ijoin :: IMonad m => m (m p) :-> m p | |
ijoin = iextend id | |
------------------------------------------------------------------------------- | |
-- IApplicative Path? | |
------------------------------------------------------------------------------- | |
data (:=) :: * -> k -> k -> * where | |
V :: (:=) a i i | |
-- List is simple, basically no index | |
type List a = Path (a := '((), ())) | |
-- But what about Vec? | |
-- | |
-- type Vec n a = Path ? | |
-- | |
-- After wandering around, you'll end up with: | |
-- | |
data Succ :: * -> (Nat, Nat) -> * where | |
Succ :: a -> Succ a '(n, 'S n) | |
type Vec a n = forall p. Path (Succ a) '(p, Plus n p) | |
-- So what about Applicatives? | |
-- Well... | |
-- | |
-- data Unit a = Unit | |
-- data (:*:) f g a = f a :*: g a | |
-- | |
-- aren't good enough. | |
type Atkey m i j a = m (a := j) i | |
-- won't work for Path as Vec | |
-- We have to write specific variant for :* | |
class IApplicativePlus m where | |
ipure :: x -> m (Succ x) '(n, 'S n) | |
-- iprod omitted - I haven't tried, it's not that easy exercise. | |
instance IApplicativePlus Path where | |
ipure x = Succ x :-: Stop | |
-- So what does this means? | |
-- | |
-- We have | |
-- | |
-- Vec :: * -> Nat -> * | |
-- | |
-- If we a monoidal product of them, having something like | |
-- | |
-- p = (x :: Vec a n, y :: Vec a m) -- monoidal product is (,) | |
-- | |
-- We want to multiply (pun unintended) the components so we get | |
-- | |
-- xy = Vec a (Mult n m) -- monoidal product is Mult | |
-- | |
-- And the latter product is specific to each instance. | |
-- There's an IApplicative for ZipList applicative for Vec, but | |
-- there product is boring. Also there is a Plus(-like) monoidal "product" | |
------------------------------------------------------------------------------- | |
-- Conclusion | |
------------------------------------------------------------------------------- | |
-- So the `indexed` approach is to take common input-output things like Path | |
-- and split the pair into two argument: | |
-- | |
-- Without an @a@ index, Path' is a Category... | |
data Path' f i o a where | |
Nil :: Path' f i i a | |
(:>>) :: f x y a -> Path' f y z a -> Path' f x z a | |
data Succ' i o a where | |
Succ' :: a -> Succ' n ('S n) a | |
type Vec' n a = forall m. Path' Succ' m (Plus m n) | |
-- and then life is easier. | |
------------------------------------------------------------------------------- | |
-- Another take | |
------------------------------------------------------------------------------- | |
-- This is awful. | |
class IApp z p f | f -> z p where | |
iunit :: a -> f z a | |
iprod :: p n m q => f n a -> f m b -> f q (a, b) | |
class Mult n m ~ q => CMult n m q | n m -> q | |
instance CMult 'Z n 'Z | |
instance (CMult n m nm, Plus m nm ~ q) => CMult ('S n) m q | |
data Dict c where | |
Dict :: c => Dict c | |
-- Vec is used as singleton | |
conjure :: V.Vec n a -> Proxy m -> Dict (CMult n m (Mult n m)) | |
conjure V.VNil _ = Dict | |
conjure (_ V.::: xs) p = case conjure xs p of | |
Dict -> Dict | |
instance IApp Nat1 CMult V.Vec where | |
iunit x = x V.::: V.VNil | |
iprod V.VNil _ = V.VNil | |
iprod (x V.::: xs) ys = iprod' (conjure xs Proxy) x xs ys where | |
iprod' :: Dict (CMult n m q) -> a -> V.Vec n a -> V.Vec m b -> V.Vec (Plus m q) (a, b) | |
iprod' Dict x xs ys = fmap ((,) x) ys V.++ iprod xs ys | |
-- >>> example | |
-- (True,'x') ::: (True,'y') ::: (True,'z') ::: (False,'x') ::: (False,'y') ::: (False,'z') ::: VNil | |
example :: V.Vec Nat6 (Bool, Char) | |
example = iprod as bs where | |
as :: V.Vec Nat2 Bool | |
as = True V.::: False V.::: V.VNil | |
bs :: V.Vec Nat3 Char | |
bs = 'x' V.::: 'y' V.::: 'z' V.::: V.VNil |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment