Skip to content

Instantly share code, notes, and snippets.

@umazalakain
Created January 25, 2021 21:23
Show Gist options
  • Save umazalakain/69384cee0c05b4a5923acb070def95d6 to your computer and use it in GitHub Desktop.
Save umazalakain/69384cee0c05b4a5923acb070def95d6 to your computer and use it in GitHub Desktop.
object LambdaCalculus {
sealed trait Type
case class Arrow[S <: Type, T <: Type]() extends Type
case class Base() extends Type
sealed trait Ctx
case class Nil() extends Ctx
case class Cons[X <: Type, XS <: Ctx]() extends Ctx
sealed trait In[T <: Type, TS <: Ctx]
case class Here[T <: Type, TS <: Ctx]() extends In[T, Cons[T,TS]]
case class There[P <: Type, T <: Type, TS <: Ctx, V <: In[T,TS]]() extends In[T, Cons[P,TS]]
sealed trait WellTyped[T <: Type, TS <: Ctx]
case class Variable[
T <: Type,
TS <: Ctx,
V <: In[T, TS]]() extends
//-------------------------
WellTyped[T, TS]
case class Abstraction[
S <: Type,
T <: Type,
TS <: Ctx,
E <: WellTyped[T, Cons[S, TS]]]() extends
//-----------------------------------------
WellTyped[Arrow[S,T], TS]
case class Application[
S <: Type,
T <: Type,
TS <: Ctx,
F <: WellTyped[Arrow[S,T], TS],
E <: WellTyped[S, TS]]() extends
//--------------------------------
WellTyped[T, TS]
def test1[T <: Type]() : WellTyped[Arrow[T,T], Nil] = Abstraction[T, T, Nil, Variable[T, Cons[T, Nil], Here[T, Nil]]]()
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment