我正在尝试在 Pie 语言（Racket）上设计代数数据类型。但仅凭我的知识我做不到

Question

#lang pie

(claim Option
  (-> U
      U))
(define Option
  (lambda (K)
    (-> K
        K)))

(claim None
  (Pi ((A U))
    (Option A)))
(define None
  (lambda (K)
    (lambda (x)
      x)))

(claim Some
  (Pi ((A U))
    (Option A)))
(define Some
  (lambda (K)
    (lambda (x)
      x)))

我无法声明“无”，并且我无法确定我所声明的内容。 那么，帮我... 我为我糟糕的英语道歉。

Answer 1

我认为你不能将

None

的类型设置为

Option

因为 Pie 没有提供数据类型或可能的东西。但是 Pie 已经有

Either

类型，所以不用创建新类型，而是可以包裹

Either

：

(claim Maybe
  (Pi ([T U]) U))
(define Maybe
  (lambda (T)
    (Either T Atom)))

(claim just
  (Pi ([T U] [t T])
    (Maybe T)))
(define just
  (lambda (T t)
    (left t)))

(claim nothing
  (Pi ([T U])
    (Maybe T)))
(define nothing
  (lambda (T)
    (right 'nothing)))

(the (Maybe Nat)
  (just Nat 1))
(the (Maybe Nat)
  (nothing Nat))