为什么Maybe / Optional类型使用Just / Some类型而不是实际类型？ [英] Why do Maybe/Optional types use a Just/Some type instead of the actual type?

问题描述

在Idris中， Maybe 类型的定义如下：

  data可能a =只是| | Nothing 
  

它在Haskell中的定义类似：

  data也许a =只是| | Nothing 
 deriving（Eq，Ord）
  

以下是ML版本：

  datatype'a option = NONE | 'a 
  

使用 Just 和某些？

为什么不在没有它们的情况下定义类型？

例子：

  data可能a = a | Nothing 
  

解决方案

然后，

 也许一个
  

和

 也许（也许a）
  

？

应该是 Nothing 和 Just Nothing 。

In Idris, the Maybe type is defined as followed:

data Maybe a = Just a | Nothing  

It's defined similarly in Haskell:

 data Maybe a = Just a | Nothing
     deriving (Eq, Ord)

Here's the ML version:

datatype 'a option = NONE | SOME of 'a

What are the benefits of using Just and Some?
Why not define the type without them?

example:

data Maybe a = a | Nothing

解决方案

What would then be the difference between

Maybe a

and

Maybe (Maybe a)

?

There's supposed to be a difference between Nothing and Just Nothing.

这篇关于为什么Maybe / Optional类型使用Just / Some类型而不是实际类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！