SystemF.idr

module SystemF

import Decidable.Equality

import Data.SnocList.Elem

namespace Kind
  public export
  data Kind : Type
    where ||| Types of Types
          Star : Kind
          ||| Type of type-level functions
          Arrow : (f,a : Kind) -> Kind


  public export
  Exists : Kind -> SnocList Kind -> Type
  Exists = Elem

  public export
  Exists' : SnocList Kind -> Kind -> Type
  Exists' ks k = Elem k ks

  public export
  Kontext : Type
  Kontext = SnocList Kind

  public export
  lift : ({l:_} -> Exists l k -> Exists l j)
      -> ({l:_} -> Exists l (k :< a) -> Exists l (j :< a))
  lift f Here = Here
  lift f (There x)
    = There (f x)

namespace Types

  namespace Value

    public export
    data Ty : Kontext -> Kind -> Type
      where
        TyVar : {k : _}
             -> Exists k ktxt
             -> Ty     ktxt k

        TyFun : {k,j : _}
             -> Ty (ktxt :< k) j
             -> Ty  ktxt (Arrow k j)

        TyApp : {k,j : _}
             -> Ty ktxt (Arrow k j)
             -> Ty ktxt        k
             -> Ty ktxt          j

        Fun : (f, a : Ty ktxt Star)
                   -> Ty ktxt Star

        Forall : {k : _}
              -> Ty (ktxt :< k) Star
              -> Ty  ktxt       Star

        Nat  : Ty ktxt Star
        Bool : Ty ktxt Star

    public export
    rename : ({l : _} -> Exists l k
                      -> Exists l j)
          -> Ty     k   a
          -> Ty       j a
    rename f (TyVar x)
      = TyVar (f x)

    rename f (TyFun x)
      = TyFun (rename (lift f) x)

    rename f (TyApp x y)
      = TyApp (rename f x)
              (rename f y)

    rename f (Fun x y)
      = Fun (rename f x)
            (rename f y)

    rename f (Forall x)
      = Forall (rename (lift f) x)

    rename f Nat
      = Nat
    rename f Bool
      = Bool

    public export
    weaken : Ty k a -> Ty (k :< j) a
    weaken = rename There

    public export
    lifts : ({j : _} -> Exists' a j
                     -> Ty      b j)
         -> ({j : _} -> Exists' (a :< k) j
                     -> Ty      (b :< k) j)
    lifts f Here
      = TyVar Here
    lifts f (There x)
      = weaken (f x)


    public export
    subst' : ({j : _} -> Exists' a j
                      -> Ty      b j)
          -> Ty a j
          -> Ty b j
    subst' f (TyVar x)
      = f x

    subst' f (TyFun x)
      = TyFun (subst' (lifts f) x)

    subst' f (TyApp x y)
      = TyApp (subst' f x)
              (subst' f y)

    subst' f (Fun x y)
      = Fun (subst' f x)
            (subst' f y)

    subst' f (Forall x)
      = Forall (subst' (lifts f) x)

    subst' f Nat
      = Nat
    subst' f Bool
      = Bool

    public export
    extend : ({j : _} ->  Exists' a j
                      -> Ty      b j)
         -> Ty b k
         -> ({j : _} ->  Exists' (a :< k) j
                     -> Ty       b       j)
    extend f x Here
      = x
    extend f x (There y)
      = f y

    public export
    subst : Ty  a    k
         -> Ty (a :< k) j
         -> Ty  a       j
    subst y
      = subst' (extend TyVar y)

  namespace NBE
    mutual

      namespace Neutral
        public export
        data Ty : Kontext
               -> Kind
               -> Type
          where
            TyVar : (idx : Exists     k ktxt)
                        -> Neutral.Ty ktxt k

            TyApp : {k,j : _}
                 -> (fun : Neutral.Ty ktxt (Arrow k j))
                 -> (arg : Normal.Ty  ktxt        k)
                        -> Neutral.Ty ktxt          j

      namespace Normal
        public export
        data Ty : Kontext
               -> Kind
               -> Type
          where
            TyFun : {k,j : _}
                 -> (param : Normal.Ty (ktxt :<     k) j)
                        -> Normal.Ty  ktxt (Arrow k  j)

            NeutralTy : {k : Kind}
                     -> Neutral.Ty ktxt k
                     -> Normal.Ty ktxt k

            Fun : (arg : Normal.Ty ktxt Star)
               -> (ret : Normal.Ty ktxt Star)
                      -> Normal.Ty ktxt Star

            Forall : {k : _}
                  -> (param : Normal.Ty (ktxt :< k) Star)
                           -> Normal.Ty  ktxt       Star

            Nat  : Normal.Ty ktxt Star
            Bool : Normal.Ty ktxt Star

    namespace Renaming
      mutual

        namespace Normal
          public export
          rename : ({l : _} -> Exists l k
                            -> Exists l j)
                -> Normal.Ty k a
                -> Normal.Ty j a
          rename f (TyFun param)
            = TyFun (rename (lift f) param)

          rename f (NeutralTy x)
            = NeutralTy (rename f x)

          rename f (Fun arg ret)
            = Fun (rename f arg)
                    (rename f ret)

          rename f (Forall param)
            = Forall (rename (lift f) param)

          rename f Nat
            = Nat

          rename f Bool
            = Bool

          public export
          weaken : Normal.Ty  ktxt       k
                -> Normal.Ty (ktxt :< j) k
          weaken = rename There

        namespace Neutral
          public export
          rename : {a : _}
                -> ({l : _} -> Exists l k
                            -> Exists l j)

                -> Neutral.Ty k a
                -> Neutral.Ty j a
          rename f (TyVar idx)
            = TyVar (f idx)

          rename f (TyApp fun arg)
            = TyApp (rename f fun)
                    (rename f arg)

    public export
    Reduce : Kontext -> Kind -> Type
    Reduce sx Star
      = Normal.Ty sx Star
    Reduce sx (Arrow f a)
      = Either (Neutral.Ty sx (Arrow f a))
               ({j : _} -> ({l : _} -> Exists l sx -> Exists l j)
                        -> Reduce j f
                        -> Reduce j a)

    public export
    reflect : {k : Kind} -- @TODO Get rid of using viiew?
           -> Neutral.Ty ktxt k
           -> Reduce     ktxt k
    reflect {k = Star} x
      = NeutralTy x

    reflect {k = (Arrow f a)} x
      = Left x

    public export
    reify : {k,ktxt : _}
         -> Reduce    ktxt k
         -> Normal.Ty ktxt k
    reify {k = Star} x
      = x
    reify {k = (Arrow y z)} (Left x)
      = NeutralTy x
    reify {k = (Arrow y z)} (Right x)
      = TyFun (reify (x There (reflect (TyVar Here))))

    public export
    rename : {s : Kind}
          -> {ktxt,jtxt : Kontext}
          -> ({i : _} -> Exists' ktxt i -> Exists' jtxt i)
          -> Reduce ktxt s
          -> Reduce jtxt s
    rename {s = Star} f x
      = rename f x

    rename {s = (Arrow y z)} f (Left x)
      = Left (rename f x)

    rename {s = (Arrow y z)} f (Right x)
      = Right (\f' => x (f' . f))

    public export
    weaken : {s : Kind}
          -> {k : Kind}
          -> {ktxt : Kontext}
          -> Reduce ktxt        s
          -> Reduce (ktxt :< k) s
    weaken = NBE.rename There

    public export
    Env : Kontext -> Kontext -> Type
    Env ktxt jtxt = {o : _} -> Exists o ktxt -> Reduce jtxt o

    public export
    ext : ({r : _} -> Exists r a -> Reduce b r)
       -> Reduce b j
       -> ({r : _ } -> Exists r (a:<j) -> Reduce b r)
    ext f x Here
      = x

    ext f x (There y) = f y


    public export
    lift : {l, ktxt, jtxt : _}
        -> ({r : _} -> Exists r ktxt -> Reduce jtxt r) -- Env ktxt jtxt
        -> ({r : _} -> Exists r (ktxt :< l) -> Reduce (jtxt :< l) r)
    lift f = ext (NBE.weaken . f) (reflect (TyVar Here))

    public export
    apply : {k,j : _}
         -> {ktxt : _}
         -> Reduce ktxt (Arrow k j)
         -> Reduce ktxt        k
         -> Reduce ktxt          j
    apply (Left x) y = reflect (TyApp x (reify y))
    apply (Right x) y = x id y

    public export
    eval : {k : Kind}
        -> {ktxt, jtxt : _}
        -> Value.Ty ktxt k
        -> ({r : _} -> Exists r ktxt -> Reduce jtxt r) -- Env    ktxt jtxt
        -> Reduce jtxt k
    eval (TyVar x) f
      =  f x

    eval (TyFun x) f
      = Right (\p, v => eval x (ext (NBE.rename p . f) v))

    eval {k} (TyApp x y) f
      = NBE.apply (eval x f)
                  (eval y f)

    eval (Fun x a) f
      = Fun (reify (eval x f))
            (reify (eval a f))

    eval (Forall x) f
      = Forall (reify (eval x
                            (NBE.lift f)
               ))

    eval Nat f
      = Nat
    eval Bool f
      = Bool


    public export
    identity : {ktxt : Kontext} -> Env ktxt ktxt
    identity = (reflect . Neutral.TyVar)

    public export
    normalise : {k : Kind}
             -> {ktxt : Kontext}
             -> Value.Ty     ktxt k
             -> Normal.Ty ktxt k
    normalise x = reify (eval x (identity))


    mutual
      public export
      embedNeu : {k : _} -> Neutral.Ty ktxt k -> Value.Ty ktxt k
      embedNeu (TyVar idx) = TyVar idx
      embedNeu (TyApp fun arg) = TyApp (embedNeu fun) (embed arg)

      public export
      embed : Normal.Ty ktxt k
           -> Value.Ty  ktxt k
      embed (TyFun param) = TyFun (embed param)
      embed (NeutralTy x) = embedNeu x

      embed (Fun arg ret) = Fun (embed arg) (embed ret)
      embed (Forall param) = Forall (embed param)
      embed Nat = Nat
      embed Bool = Bool


    namespace Subst

      public export
      lift : ({ k : _} -> Exists k a -> Normal.Ty b k)
          -> ({ k : _} -> Exists k (a :< j) -> Normal.Ty (b :< j) k)
      lift f Here
        = NeutralTy (TyVar Here)
      lift f (There x)
        = weaken (f x)

      public export
      extend : ({ k : _} -> Exists k a -> Normal.Ty b k)
            -> Normal.Ty b j
            -> ({ k : _} -> Exists k (a :< j) -> Normal.Ty b k)
      extend f x Here
        = x
      extend f x (There y)
        = f y

      public export
      subst' : {a,b,j : _}
            -> ({ r : _} -> Exists r a -> Normal.Ty b r)
            -> Normal.Ty a j
            -> Normal.Ty b j
      subst' x f
        = normalise (subst' (embed . x) (embed f))

      public export
      subst : {k,j,a : _}
           -> Normal.Ty  a    k
           -> Normal.Ty (a :< k) j
           -> Normal.Ty  a       j
      subst x y
        = subst' (extend (NeutralTy . TyVar) x)
                 y

namespace Terms

  public export
  data Context : Kontext -> Type where
   Empty : Context [<]
   ExtKind : Context ks -> Context (ks :< k)
   ExtType : Context ks -> Normal.Ty ks Star -> Context ks

  public export
  data IsType : Context ks -> Normal.Ty ks Star -> Type
    where
      Here : IsType (ExtType ks ty) ty

      IsKind : IsType ks ty
            -> IsType (ExtKind ks) (weaken ty)

      There : IsType          ks      ty
           -> IsType (ExtType ks ty') ty

  public export
  data Term : Context k -> Normal.Ty k Star -> Type where
    Zero : Term g Nat
    Succ : Term g Nat -> Term g Nat
    True,False : Term g Bool

    Var : IsType g ty -> Term g ty
    Fun : Term (ExtType g a) b
       -> Term          g    (Fun a b)

    App : Term g (Fun a b)
       -> Term g      a
       -> Term g        b

    Forall : Term (ExtKind g) b
          -> Term          g  (Forall b)

    Resolve : (body  : Term      g (Forall b))
           -> (this  : Normal.Ty ks k)
                    -> Term      g (subst this b)

identity : Term Empty (Forall (Fun (NeutralTy (TyVar Here))
                                   (NeutralTy (TyVar Here))))
identity
  = Forall
    $ Fun
      $ (Var Here)

natIdentity : Term Empty (Fun Nat Nat)
natIdentity
  = Resolve identity Nat