小编Lia*_*cre的帖子

伊德里斯版: 0.9.16

我试图描述从base值和迭代step函数生成的构造:

namespace Iterate
  data Iterate : (base : a) -> (step : a -> a) -> a -> Type where
    IBase : Iterate base step base
    IStep : Iterate base step v -> Iterate base step (step v)

使用这个我可以定义Plus,描述迭代添加jump值的构造:

namespace Plus
  Plus : (base : Nat) -> (jump : Nat) -> Nat -> Type
  Plus base jump = Iterate base (\v => jump + v)

这个的简单示例用法:

namespace PlusExamples
  Even : …

我正在玩Haskell,并认为我会尝试用它创建一个简单的编程语言.暂时忽略具体语法; 我专注于抽象语法和语义.

语言当前应包含整数,整数加法,变量名和变量绑定块.

如果使用的是在使用范围内不存在的变量,则会引发错误.

以下是我目前的进展:

module ProgLang where
import Data.Map as Map

--  Classes
class Runnable d where
  run :: (Runnable a) => d -> Map String a -> Either [String] Integer

--  Data
data Name = Name String
  deriving (Eq, Ord, Show)

data Add a b = Add a b
  deriving (Eq, Ord, Show)

data Block a = Block (Map String a) a
  deriving (Eq, Ord, Show)

--  Instances
--  Integers resolve to Right Integer
instance Runnable Integer where …