Haskell类型的构造函数可以不是

2018-06-15 04:00:58

类型构造函数产生给定类型的类型。例如，Maybe构造函数

data Maybe a = Nothing | Just a

可以是给定的具体类型，如Char，并给出具体类型，如Maybe Char。就种类而言，有一个

GHCI> :k Maybe
Maybe :: * -> *

我的问题：是否有可能定义一个类型构造函数产生一个具体的类型给予一个字符，说？换句话说，是否可以在类型构造函数的类型签名中混合种类和类型？就像是

GHCI> :k my_type
my_type :: Char -> * -> *

Haskell类型的构造函数是否有非类型参数？

让我们按类型参数解开你的意思。 Word类型有（至少）两个潜在的意思：你的意思是在事物的狭义型样* ，或者事情在类型级别的更广泛的意义？我们不能（在）类型中使用值，但现代GHC具有非常丰富的类型语言，允许我们使用除具体类型之外的各种各样的东西作为类型参数。

高端类型

Haskell中的类型构造函数一直承认非*参数。例如，一个函数的固定点的编码在普通的旧Haskell 98中工作：

newtype Fix f = Fix { unFix :: f (Fix f) }

ghci> :k Fix
Fix :: (* -> *) -> *

Fix由一个类* -> *的函子进行参数化，而不是一种类型* 。

超越`*`和`->`

DataKinds扩展使用用户声明的类型丰富了GHC的类系统，因此可以用*和->以外的部分构建类型。它通过将所有data声明提升到种类级别来工作。也就是说，像一个data声明

data Nat = Z | S Nat  -- natural numbers

引入了一种Nat和类型构造函数Z :: Nat和S :: Nat -> Nat ，以及通常的类型和值构造函数。这使您可以编写通过类型级别数据进行参数化的数据类型，例如通常的矢量类型，这是一种按其长度索引的链接列表。

data Vec n a where
    Nil :: Vec Z a
    (:>) :: a -> Vec n a -> Vec (S n) a

ghci> :k Vec
Vec :: Nat -> * -> *

有一个名为ConstraintKinds的相关扩展，它可以像Ord a从“fat arrow” =>的轭中释放约束，使它们能够像自然界所期望的那样在类型系统的环境中漫游。 Kmett利用这种力量来构建一类约束，用newtype (:-) :: Constraint -> Constraint -> *表示“entailment”：类型c :- d的值c :- d是一个证明，如果c成立，那么d也持有。例如，我们可以证明Ord a对所有a都意味着Eq [a] ：

ordToEqList :: Ord a :- Eq [a]
ordToEqList = Sub Dict

之后的新生活`forall`

但是，Haskell目前在类型级别和值级别之间保持严格分离。事情在类型级别总是删除该程序运行之前，（几乎）总是inferrable，在表达无形的，（依赖）的量化forall 。如果你的应用程序需要更灵活的东西，比如运行时数据的依赖量化，那么你必须使用单例编码手动模拟它。

例如， split的规格说明它根据它的（运行时！）参数在一定长度上截断一个向量。输出向量的类型取决于split参数的值。我们想写这个...

split :: (n :: Nat) -> Vec (n :+: m) a -> (Vec n a, Vec m a)

...我使用类型函数(:+:) :: Nat -> Nat -> Nat ，它代表添加类型级别的自然函数，以确保输入向量至少与n一样长。 ..

type family n :+: m where
    Z :+: m = m
    S n :+: m = S (n :+: m)

...但Haskell不会允许split声明！没有任何类型的Z或S n ; 只有类型*包含值。我们不能直接在运行时访问n ，但我们可以使用一个我们可以进行模式匹配的GADT来了解类型n是什么：

data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

ghci> :k Natty
Natty :: Nat -> *

Natty被称为单例，因为对于给定的（明确定义的） n ，只有一个（明确定义的）类型的值Natty n 。我们可以用Natty n作为运行时间替身n 。

split :: Natty n -> Vec (n :+: m) a -> (Vec n a, Vec m a)
split Zy xs = (Nil, xs)
split (Sy n) (x :> xs) =
    let (ys, zs) = split n xs
    in (x :> ys, zs)

无论如何，重点是值 - 运行时数据 - 不能出现在类型中。以单例形式复制Nat的定义非常繁琐（如果你希望编译器推断出这样的值，事情会变得更糟）。像Agda，Idris或未来的Haskell这样的依赖类型的语言可以摆脱严格区分类型与值的暴政，并为我们提供一系列富有表现力的量词。您可以使用诚实善良的Nat作为split的运行时参数，并在返回类型中独立提及它的值。

@pigworker写了很多关于Haskell在现代依赖类型编程的类型和值之间严格区分的不适用性。例如，参见Hasochism论文，或者他关于四十年辛德雷 - 米尔纳式编程的未经考虑的假设的演讲。

依赖种类

最后，对于它的价值，使用TypeInType现代GHC统一了类型和类型，允许我们使用我们用于讨论类型变量的相同工具来讨论类变量。在之前关于会话类型的文章中，我使用TypeInType为标记的类型级别序列类型定义了一种类型：

infixr 5 :!, :?
data Session = Type :! Session  -- Type is a synonym for *
             | Type :? Session
             | E

我推荐@Benjamin Hodgson的回答以及他提供的参考资料，以了解如何使这类事情有用。但是，要使用多个扩展（ DataKinds ， KindSignatures和GADTs ）更直接地回答您的问题，可以定义在（某些）具体类型上参数化的类型。

例如，下面是一个在具体Bool数据类型上参数化的例子：

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
{-# LANGUAGE FlexibleInstances #-}

module FlaggedType where

-- The single quotes below are optional.  They serve to notify
-- GHC that we are using the type-level constructors lifted from
-- data constructors rather than types of the same name (and are
-- only necessary where there's some kind of ambiguity otherwise).
data Flagged :: Bool -> * -> * where
  Truish  :: a -> Flagged 'True a
  Falsish :: a -> Flagged 'False a

-- separate instances, just as if they were different types
-- (which they are)
instance (Show a) => Show (Flagged 'False a) where
  show (Falsish x) = show x
instance (Show a) => Show (Flagged 'True a) where
  show (Truish x) = show x ++ "*"

-- these lists have types as indicated
x = [Truish 1, Truish 2, Truish 3]           -- :: Flagged 'True Integer
y = [Falsish "a", Falsish "b", Falsish "c"]  -- :: Flagged 'False String

-- this won't typecheck: it's just like [1,2,"abc"]
z = [Truish 1, Truish 2, Falsish 3]          -- won't typecheck

请注意，这与定义两个完全独立的类型没有多大区别：

data FlaggedTrue a = Truish a
data FlaggedFalse a = Falsish a

实际上，我很难想出Flagged在定义两种不同类型方面的优势，除非你有一个酒吧赌注，你可以在没有类型类的情况下编写有用的Haskell代码。例如，你可以写：

getInt :: Flagged a Int -> Int
getInt (Truish z) = z    -- same polymorphic function...
getInt (Falsish z) = z   -- ...defined on two separate types

也许别人可以想到其他一些优点。

无论如何，我相信只要具体类型足够“丰富”，您就可以用它来利用类型检查器，那么使用具体值的参数化类型才会有用，就像本杰明的例子。

正如@ user2407038指出的那样，大多数有趣的基本类型，如Int ， Char ， String等都不能用这种方式。有趣的是，尽管可以使用文字正整数和字符串作为类型参数，但它们分别被当作Nat和Symbol s（在GHC.TypeLits定义）。

所以这样的事情是可能的：

import GHC.TypeLits
data Tagged :: Symbol -> Nat -> *  -> * where
    One :: a -> Tagged "one" 1 a
    Two :: a -> Tagged "two" 2 a
    Three :: a -> Tagged "three" 3 a

请看使用通用代数数据类型（GADTS），它们使您能够根据输入类型定义具体的输出，例如

data CustomMaybe a where
  MaybeChar :: Maybe a -> CustomMaybe Char
  MaybeString :: Maybe a > CustomMaybe String
  MaybeBool :: Maybe a -> CustomMaybe Bool

exampleFunction :: CustomMaybe a -> a
exampleFunction (MaybeChar maybe) = 'e' 
exampleFunction (MaybeString maybe) = True //Compile error

main = do 
  print $ exampleFunction (MaybeChar $ Just 10)

为了达到类似的效果，RankNTypes可以允许执行类似的行为：

exampleFunctionOne :: a -> a
exampleFunctionOne el = el

type PolyType = forall a. a -> a

exampleFuntionTwo :: PolyType -> Int
exampleFunctionTwo func = func 20
exampleFunctionTwo func = func "Hello" --Compiler error, PolyType being forced to return 'Int'

main = do
  print $ exampleFunctionTwo exampleFunctionOne

PolyType定义允许您在exampleFunctionTwo中插入多态函数并强制其输出为'Int'。

链接地址: http://www.djcxy.com/p/43061.html

上一篇: Can a Haskell type constructor have non

下一篇: Finding type signatures in Haskell

Haskell类型的构造函数可以不是

高端类型

超越*和->

之后的新生活forall

依赖种类

超越`*`和`->`

之后的新生活`forall`