Trying to write an interpreter function over HList of Exp

Stream: lean4

[James Good]

Hello,

I was working through a compiler book that uses Racket.

However, I don't fancy dynamic types, so I wanted to see if I could implement the designs they present in the book in a dependently typed language.

I started off using Idris2 awhile back, but I've switched to learning Lean recently and attempted to port over what little I had started on.

I can't get the interpreter function in Lean to compile, however, it compiles and runs just fine in Idris2.

Here's the Idris2 code:

module MinInterp

import Data.String

------------------------------------------------------------
-- Define Expression Types
record IntExp where
  constructor MkIntExp
  x : Int

record BoolExp where
  constructor MkBoolExp
  x : Bool

record StringExp where
  constructor MkStringExp
  x : String


-----------------------------------------------------------
-- Define `HList`

data HList : List Type -> Type where
  HNil  : HList Nil
  (:::) : {t : Type} -> t -> HList ts -> HList (t :: ts)

infixr 5 :::


-----------------------------------------------------------
-- Define Primitive Operations

record Prim (e : List Type) where
  constructor MkPrim
  op      : String
  args    : HList e

-- Example instances
eight : IntExp
eight = MkIntExp 8

neg_eight : Prim [IntExp]
neg_eight = MkPrim "-" (eight ::: HNil)

rd : Prim Nil
rd = MkPrim "read" HNil



----------------------------------------------
-- Define Result Type

data Result : Type where
  IntResult : Int -> Result
  BoolResult : Bool -> Result
  StringResult : String -> Result

Show Result where
  show (IntResult i) = "IntResult " ++ show i
  show (BoolResult b) = "BoolResult " ++ show b
  show (StringResult s) = "StringResult \"" ++ s ++ "\""


----------------------------------------------
-- Define Interpreter
interpPrim : Prim e -> Maybe Result
interpPrim (MkPrim "read" HNil) = Just (IntResult 42) -- Replace with actual read operation
interpPrim (MkPrim "-" (MkIntExp x ::: HNil)) = Just (IntResult (-x))
interpPrim (MkPrim "+" (MkIntExp x ::: MkIntExp y ::: HNil)) = Just (IntResult (x + y))
interpPrim (MkPrim "-" (MkIntExp x ::: MkIntExp y ::: HNil)) = Just (IntResult (x - y))
interpPrim _ = Nothing


main : IO ()
main = do
  let x = interpPrim neg_eight
  putStrLn (show x)

And here's the Lean4 code:

------------------------------------------------------------
-- Define Expression Types

structure IntExp where
  x : Int
deriving Repr

structure BoolExp where
  x : Bool
deriving Repr

structure StringExp where
  x : String
deriving Repr


-----------------------------------------------------------
-- Define `HList`

inductive HList : List Type → Type 1 where -- fails to compile without the '1' in 'Type 1'
  | nil : HList []
  | cons : {t : Type} → t → HList ts → HList (t :: ts)

infixr:5 " ::: " => HList.cons


-----------------------------------------------------------
-- Define Primitive Operations

structure Prim (e : List Type) where
  operation : String
  arguments : HList e

def eight : IntExp := IntExp.mk 8

def neg_eight : Prim [IntExp] := Prim.mk "-" (eight ::: HList.nil)

def rd : Prim [] := Prim.mk "read" HList.nil



----------------------------------------------
-- Define Result Type

inductive Result where
  | int_result : Int -> Result
  | BoolResult : Bool -> Result
  | StringResult : String -> Result
deriving Repr



----------------------------------------------
-- Define Interpreter

-- Doesn't compile:
-- Line that has the pattern match ({ x := 9001 } : Int Exp) :: HList.nil
-- fails to compile with the following error message:
-- pattern
--   { x := _fvar.5221 }
-- has type
--   IntExp : Type
-- but is expected to have type
--   t✝ : Type
def interpret_prim : {e: List Type} → Prim e → Option Result
  | _, { operation := "read", arguments := HList.nil } => some $ Result.int_result 42 -- replace with actual read operation
  | _, { operation := "-", arguments := ((IntExp.mk a) ::: HList.nil) } => some $ Result.int_result a
  | _, { operation := _, arguments := _ } => none

#eval interpret_prim neg_eight

Is there no way to get this to compile?

[Mario Carneiro]

you can define HList to avoid a universe bump but you need to define it by recursion instead of induction

[Mario Carneiro]

here's a version which uses a recursive definition of HList:

-----------------------------------------------------
-- Define Expression Types

structure IntExp where
  x : Int
deriving Repr

structure BoolExp where
  x : Bool
deriving Repr

structure StringExp where
  x : String
deriving Repr


-----------------------------------------------------------
-- Define `HList`

def HList : List Type → Type
  | [] => Unit
  | t :: ts => t × HList ts


-----------------------------------------------------------
-- Define Primitive Operations

structure Prim (e : List Type) where
  operation : String
  arguments : HList e

def eight : IntExp := IntExp.mk 8

def neg_eight : Prim [IntExp] := Prim.mk "-" (eight, ())

def rd : Prim [] := Prim.mk "read" ()



----------------------------------------------
-- Define Result Type

inductive Result where
  | int_result : Int -> Result
  | BoolResult : Bool -> Result
  | StringResult : String -> Result
deriving Repr



----------------------------------------------
-- Define Interpreter

def interpret_prim : {e: List Type} → Prim e → Option Result
  | [], { operation := "read", arguments := () } => some $ Result.int_result 42 -- replace with actual read operation
  | .([IntExp]), { operation := "-", arguments := (IntExp.mk a, ()) } => some $ Result.int_result a
  | _, { operation := _, arguments := _ } => none

#eval interpret_prim neg_eight

[Mario Carneiro]

However, it doesn't fix the main issue, and I think you can't really do this in lean. The trouble is that in your second pattern match, the expression ((IntExp.mk a) ::: HList.nil) forces a certain type for e: List Type, which is to say the _ is actually [IntExp] here, but while you can pattern match the List Type to have form [_], you can't use pattern matching to make it IntExp without deciding type equality.

[Mario Carneiro]

The right solution to this is the universe pattern

[Mario Carneiro]

-----------------------------------------------------
-- Define Expression Types

structure IntExp where
  x : Int
deriving Repr

structure BoolExp where
  x : Bool
deriving Repr

structure StringExp where
  x : String
deriving Repr

inductive TypeCode where
  | int
  | bool
  | string

def TypeCode.toExp : TypeCode → Type
  | .int => IntExp
  | .bool => BoolExp
  | .string => StringExp

-----------------------------------------------------------
-- Define `HList`

def HList : List TypeCode → Type
  | [] => Unit
  | t :: ts => t.toExp × HList ts

-----------------------------------------------------------
-- Define Primitive Operations

structure Prim (e : List TypeCode) where
  operation : String
  arguments : HList e

def eight : IntExp := IntExp.mk 8

def neg_eight : Prim [.int] := Prim.mk "-" (eight, ())

def rd : Prim [] := Prim.mk "read" ()



----------------------------------------------
-- Define Result Type

inductive Result where
  | int_result : Int -> Result
  | BoolResult : Bool -> Result
  | StringResult : String -> Result
deriving Repr



----------------------------------------------
-- Define Interpreter

def interpret_prim : {e: List TypeCode} → Prim e → Option Result
  | [], { operation := "read", arguments := () } => some $ Result.int_result 42 -- replace with actual read operation
  | [.int], { operation := "-", arguments := (IntExp.mk a, ()) } => some $ Result.int_result a
  | _, { operation := _, arguments := _ } => none

#eval interpret_prim neg_eight

[James Good]

Mario Carneiro said:

The right solution to this is the universe pattern

Thank you for taking the time to reply.

I can understand why this shouldn't work after seeing the explanation, regarding the identity function, as to why you wouldn't want to pattern match on types.

However, I suppose my initial reason for expecting it to work is because the Idris2 version does compile, whereas the Lean4 version does not.

I'll have to give chapter 8 of the Functional Programming in Lean book a read.

[Yuri]

Out of curiosity, what is the underlying reason why Idris compiles the original code fine and Lean doesn't?

[Mario Carneiro]

maybe @David Thrane Christiansen knows?

[David Thrane Christiansen]

I'm a bit out of the loop on modern Idris, but my understanding is that pattern matching the universe is allowed. Type erasure and something akin to parametricity (don't know if it is exactly that or not) is then achieved through the quantity system, by declaring them irrelevant. This is just a vague recollection, though - a quick search didn't point me to anywhere in the docs that describes this in particular.