Can a Haskell type constructor have non

2018-06-15 04:00:58

A type constructor produces a type given a type. For example, the Maybe constructor

data Maybe a = Nothing | Just a

could be a given a concrete type, like Char, and give a concrete type, like Maybe Char. In terms of kinds, one has

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

My question: Is it possible to define a type constructor that yields a concrete type given a Char, say? Put another way, is it possible to mix kinds and types in the type signature of a type constructor? Something like

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

Can a Haskell type constructor have non-type parameters?

Let's unpack what you mean by type parameter. The word type has (at least) two potential meanings: do you mean type in the narrow sense of things of kind * , or in the broader sense of things at the type level? We can't (yet) use values in types, but modern GHC features a very rich kind language, allowing us to use a wide range of things other than concrete types as type parameters.

Higher-Kinded Types

Type constructors in Haskell have always admitted non- * parameters. For example, the encoding of the fixed point of a functor works in plain old Haskell 98:

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

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

Fix is parameterised by a functor of kind * -> * , not a type of kind * .

Beyond `*` and `->`

The DataKinds extension enriches GHC's kind system with user-declared kinds, so kinds may be built of pieces other than * and -> . It works by promoting all data declarations to the kind level. That is to say, a data declaration like

data Nat = Z | S Nat  -- natural numbers

introduces a kind Nat and type constructors Z :: Nat and S :: Nat -> Nat , as well as the usual type and value constructors. This allows you to write datatypes parameterised by type-level data, such as the customary vector type, which is a linked list indexed by its length.

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

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

There's a related extension called ConstraintKinds , which frees constraints like Ord a from the yoke of the "fat arrow" => , allowing them to roam across the landscape of the type system as nature intended. Kmett has used this power to build a category of constraints, with the newtype (:-) :: Constraint -> Constraint -> * denoting "entailment": a value of type c :- d is a proof that if c holds then d also holds. For example, we can prove that Ord a implies Eq [a] for all a :

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

Life after `forall`

However, Haskell currently maintains a strict separation between the type level and the value level. Things at the type level are always erased before the program runs, (almost) always inferrable, invisible in expressions, and (dependently) quantified by forall . If your application requires something more flexible, such as dependent quantification over runtime data, then you have to manually simulate it using a singleton encoding.

For example, the specification of split says it chops a vector at a certain length according to its (runtime!) argument. The type of the output vector depends on the value of split 's argument. We'd like to write this...

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

... where I'm using the type function (:+:) :: Nat -> Nat -> Nat , which stands for addition of type-level naturals, to ensure that the input vector is at least as long as n ...

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

... but Haskell won't allow that declaration of split ! There aren't any values of type Z or S n ; only types of kind * contain values. We can't access n at runtime directly, but we can use a GADT which we can pattern-match on to learn what the type-level n is:

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

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

Natty is called a singleton, because for a given (well-defined) n there is only one (well-defined) value of type Natty n . We can use Natty n as a run-time stand-in for 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)

Anyway, the point is that values - runtime data - can't appear in types. It's pretty tedious to duplicate the definition of Nat in singleton form (and things get worse if you want the compiler to infer such values); dependently-typed languages like Agda, Idris, or a future Haskell escape the tyranny of strictly separating types from values and give us a range of expressive quantifiers. You're able to use an honest-to-goodness Nat as split 's runtime argument and mention its value dependently in the return type.

@pigworker has written extensively about the unsuitability of Haskell's strict separation between types and values for modern dependently-typed programming. See, for example, the Hasochism paper, or his talk on the unexamined assumptions that have been drummed into us by four decades of Hindley-Milner-style programming.

Dependent Kinds

Finally, for what it's worth, with TypeInType modern GHC unifies types and kinds, allowing us to talk about kind variables using the same tools that we use to talk about type variables. In a previous post about session types I made use of TypeInType to define a kind for tagged type-level sequences of types:

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

I'd recommend @Benjamin Hodgson's answer and the references he gives to see how to make this sort of thing useful. But, to answer your question more directly, using several extensions ( DataKinds , KindSignatures , and GADTs ), you can define types that are parameterized on (certain) concrete types.

For example, here's one parameterized on the concrete Bool datatype:

{-# 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

Note that this isn't much different from defining two completely separate types:

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

In fact, I'm hard pressed to think of any advantage Flagged has over defining two separate types, except if you have a bar bet with someone that you can write useful Haskell code without type classes. For example, you can write:

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

Maybe someone else can think of some other advantages.

Anyway, I believe that parameterizing types with concrete values really only becomes useful when the concrete type is sufficient "rich" that you can use it to leverage the type checker, as in Benjamin's examples.

As @user2407038 noted, most interesting primitive types, like Int s, Char s, String s and so on can't be used this way. Interestingly enough, though, you can use literal positive integers and strings as type parameters, but they are treated as Nat s and Symbol s (as defined in GHC.TypeLits ) respectively.

So something like this is possible:

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

Look at using Generalized Algebraic Data Types (GADTS), which enable you to define concrete outputs based on input type, eg

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)

To a similar effect, RankNTypes can allow the implementation of similar behaviour:

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

The PolyType definition allows you to insert the polymorphic function within exampleFunctionTwo and force its output to be 'Int'.

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

上一篇: 派生`Eq`实例真* O（N）*？

下一篇: Haskell类型的构造函数可以不是

Can a Haskell type constructor have non

Higher-Kinded Types

Beyond * and ->

Life after forall

Dependent Kinds

Beyond `*` and `->`

Life after `forall`