Skip to content

Instantly share code, notes, and snippets.

@phadej
Last active June 16, 2019 21:11
Show Gist options
  • Save phadej/f491dfc7fe2d3e0a2f040915f7310fb0 to your computer and use it in GitHub Desktop.
Save phadej/f491dfc7fe2d3e0a2f040915f7310fb0 to your computer and use it in GitHub Desktop.
Someone asked whether you can model SystemF(omega) in Haskell. I think you can.
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeApplications #-}
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import GHC.Exts (Any)
-------------------------------------------------------------------------------
-- Elem
-------------------------------------------------------------------------------
data Elem (x :: k) (xs :: [k]) where
Here :: Elem x (x ': xs)
There :: Elem x xs -> Elem x (y ': xs)
data SElem (x :: k) (xs :: [k]) (e :: Elem x xs) where
SHere :: SElem x (x ': xs) 'Here
SThere :: SElem x xs e -> SElem x (y ': xs) ('There e)
weakenElem
:: SList ctx1
-> Proxy ctx2
-> Proxy ki
-> Elem a (Append ctx1 ctx2)
-> Elem a (Append ctx1 (ki : ctx2))
weakenElem SNil _ _ i = There i
weakenElem (SCons _) _ _ Here = Here
weakenElem (SCons ctx1) ctx2 ki (There i) = There (weakenElem ctx1 ctx2 ki i)
-------------------------------------------------------------------------------
-- Sigma
-------------------------------------------------------------------------------
data Sigma (f :: k -> Type) (g :: k -> Type) where
Exists :: f k -> g k -> Sigma f g
-------------------------------------------------------------------------------
-- List
-------------------------------------------------------------------------------
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys
data SList :: [k] -> Type where
SNil :: SList '[]
SCons :: SList xs -> SList (x ': xs)
-------------------------------------------------------------------------------
-- Kinds
-------------------------------------------------------------------------------
-- kinds
data Ki
= KiStar
| KiArrow Ki Ki
-- kind singletons
data SKi :: Ki -> Type where
SKiStar :: SKi 'KiStar
SKiArrow :: SKi a -> SKi b -> SKi ('KiArrow a b)
-- kind singleton singletons
data SSKi (ki :: Ki) (ski :: SKi ki) :: Type where
SSKiStar :: SSKi 'KiStar 'SKiStar
SSKiArrow :: SSKi a sa
-> SSKi b sb
-> SSKi ('KiArrow a b) ('SKiArrow sa sb)
-------------------------------------------------------------------------------
-- Types
-------------------------------------------------------------------------------
type KiCtx = [Ki]
-- | Types are in a normal form, even we have TyLam.
data Ty (kictx :: KiCtx) (ki :: Ki) :: Type where
TyNeutral :: TyNeutral kictx ki -> Ty kictx ki
TyLam :: Ty (ka ': kictx) kb -> Ty kictx ('KiArrow ka kb)
TyArr :: Ty kictx 'KiStar -> Ty kictx 'KiStar -> Ty kictx 'KiStar
data TyNeutral (kictx :: KiCtx) (ki :: Ki) :: Type where
TyVar :: Elem ki kictx -> TyNeutral kictx ki
TyApp :: TyNeutral kictx ('KiArrow ka kb)
-> Ty kictx ka
-> TyNeutral kictx kb
-- example
ex1 :: Sigma SKi (Ty '[ 'KiStar ])
ex1 = Exists SKiStar (TyNeutral (TyVar Here))
-------------------------------------------------------------------------------
-- Types singleton
-------------------------------------------------------------------------------
data STy (kictx :: KiCtx) (ki :: Ki) (ty :: Ty kictx ki) :: Type where
STyNeutral :: STyNeutral kictx ki x
-> STy kictx ki ('TyNeutral x)
STyLam :: STy (ka ': kictx) kb x
-> STy kictx ('KiArrow ka kb) ('TyLam x)
STyArr :: STy kictx 'KiStar a
-> STy kictx 'KiStar b
-> STy kictx 'KiStar ('TyArr a b)
data STyNeutral (kictx :: KiCtx) (ki :: Ki) (ty :: TyNeutral kictx ki) :: Type where
STyVar :: SElem ki kictx x
-> STyNeutral kictx ki ('TyVar x)
STyApp :: STyNeutral kictx ('KiArrow ka kb) f
-> STy kictx ka x
-> STyNeutral kictx kb ('TyApp f x)
-------------------------------------------------------------------------------
-- Weakening
-------------------------------------------------------------------------------
weakenKindN :: SList ctx1
-> Proxy ctx2
-> Proxy ki
-> TyNeutral (Append ctx1 ctx2) a
-> TyNeutral (Append ctx1 (ki ': ctx2)) a
weakenKindN ctx1 ctx2 ki (TyVar e) = TyVar (weakenElem ctx1 ctx2 ki e)
weakenKindN ctx1 ctx2 ki (TyApp f x) = TyApp (weakenKindN ctx1 ctx2 ki f) (weakenKind ctx1 ctx2 ki x)
weakenKind :: SList ctx1
-> Proxy ctx2
-> Proxy ki
-> Ty (Append ctx1 ctx2) a
-> Ty (Append ctx1 (ki ': ctx2)) a
weakenKind ctx1 ctx2 ki (TyNeutral n) = TyNeutral (weakenKindN ctx1 ctx2 ki n)
weakenKind ctx1 ctx2 ki (TyLam ty) = TyLam (weakenKind (SCons ctx1) ctx2 ki ty)
weakenKind ctx1 ctx2 ki (TyArr a b) = TyArr (weakenKind ctx1 ctx2 ki a) (weakenKind ctx1 ctx2 ki b)
-------------------------------------------------------------------------------
-- Type applications
-------------------------------------------------------------------------------
tySubstV :: SList ctx1
-> Ty ctx2 a
-> Elem b (Append ctx1 (a ': ctx2))
-> Ty (Append ctx1 ctx2) b
tySubstV SNil s Here = s
tySubstV SNil _ (There i) = TyNeutral (TyVar i)
tySubstV (SCons _) _ Here = TyNeutral (TyVar Here)
tySubstV (SCons c) s (There i) = weakenKind SNil Proxy Proxy $ tySubstV c s i
tySubstN :: SList ctx1
-> Ty ctx2 a
-> TyNeutral (Append ctx1 (a ': ctx2)) b
-> Ty (Append ctx1 ctx2) b
tySubstN p s (TyVar v) = tySubstV p s v
tySubstN p s (TyApp f x) = tyApp (tySubstN p s f) (tySubst p s x)
tySubst :: SList ctx1
-> Ty ctx2 a
-> Ty (Append ctx1 (a ': ctx2)) b
-> Ty (Append ctx1 ctx2) b
tySubst p s (TyNeutral n) = tySubstN p s n
tySubst p s (TyLam body) = TyLam $ tySubst (SCons p) s body
tySubst p s (TyArr a b) = TyArr (tySubst p s a) (tySubst p s b)
-- we'll need a version of this (and tySubst) on type level,
-- i.e. working with singleton of Ty. "fun".
tyApp :: Ty kictx ('KiArrow ka kb) -> Ty kictx ka -> Ty kictx kb
tyApp (TyNeutral f) x = TyNeutral (TyApp f x)
tyApp (TyLam body) x = tySubst SNil x body
-------------------------------------------------------------------------------
-- tyApp family: TyAppF
-------------------------------------------------------------------------------
type family TyAppF (a :: Ty ictx ('KiArrow ka kb)) (b :: Ty kictx ka) :: Ty kictx kb where
TyAppF ('TyNeutral f) x = 'TyNeutral ('TyApp f x)
TyAppF ('TyLam body) x = Any -- TODO
{- TODO: following doesn't work
8.6.5
• Illegal type synonym family application in instance: 'TyArr aa bb
• In the equations for closed type family ‘TySubstF’
In the type family declaration for ‘TySubstF’
8.8.1
• Illegal type synonym family application ‘Append
@Ki ctx1 ((':) @Ki a ctx2)’ in instance:
TySubstF
@ctx2
@a
@'KiStar
ctx1
s
('TyArr @(Append @Ki ctx1 ((':) @Ki a ctx2)) aa bb)
• In the equations for closed type family ‘TySubstF’
In the type family declaration for ‘TySubstF’
-}
type family TySubstF (ctx1 :: [Ki]) (s :: Ty ctx2 a) (x :: Ty (Append ctx1 (a ': ctx2)) b) :: Ty (Append ctx1 ctx2) b where
TySubstF ctx1 s ('TyArr aa bb) = 'TyArr (TySubstF ctx1 s aa) (TySubstF ctx1 s bb)
-------------------------------------------------------------------------------
-- Terms / Expressions
-------------------------------------------------------------------------------
type TyCtx (kictx :: KiCtx) = [Sigma SKi (Ty kictx)]
data Expr (kictx :: KiCtx) (tyctx :: TyCtx kictx) (ki :: Ki) (ty :: Ty kictx ki) :: Type where
Var :: SSKi ki ski -> Elem ('Exists ski ty) tyctx -> Expr kictx tyctx ki ty
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment