Create data constructor for partially applied type in Haskell

Question

Is it possible to create a data constructor for partially applied type in Haskell?

ghci session:

Prelude> data Vector a b = Vector {x::a, y::b}
Prelude> :t Vector
Vector :: a -> b -> Vector a b
Prelude> type T1 = Vector Int
Prelude> :t T1
<interactive>:1:1: Not in scope: data constructor `T1'
Prelude> let x = Vector
Prelude> let y = T1
<interactive>:46:9: Not in scope: data constructor `T1'

I want to create data constructor for type T1 - is it even possible? Or do I have to use newtypes, because it is not possible to manually define such function?

Answer 1

I'm a little confused as to what your goal is, but let's go through this bit by bit, and maybe I'll hit the right point:

:t tells you the type of a variable; it makes no sense when applied to a type, since it would just return exactly what you passed. Notice the errors here tell you that :t expects some kind of data value as a parameter:

Prelude> :t Maybe

<interactive>:1:1: Not in scope: data constructor `Maybe'
Prelude> :t (Maybe Integer)

<interactive>:1:2: Not in scope: data constructor `Maybe'

<interactive>:1:8: Not in scope: data constructor `Integer'

You can create a partial type:

Prelude> type T = Maybe
Prelude> Just 5 :: T Integer
Just 5

type T a = Maybe a -- alternately, with explicit type parameters
Prelude> Just 'a' :: T Char
Just 'a'

You can't create a data constructor for a partial type, since they don't represent data. What values could a Maybe or Vector have without being parameterized on a type? You might be inclined to think that Maybe could have the value Nothing, but Nothing is typed as:

Prelude> :t Nothing
Nothing :: Maybe a

The key being that Nothing can be any Maybe a, but it still needs an a to know it's Nothing. (It's sort of like if I told you "fetch me a glass of" instead of "fetch me a glass of anything" - you can't validly comply until I've at least finished my thought).

You can certainly create partially applied functions which will return a complete type once they're applied:

Prelude> let f = Just :: a -> T a
Prelude> f 5
Just 5
Prelude> :t f 'a'
f 'a' :: T Char

Answer 2

GADTs can do this. GHCi session:

λ :set -XGADTs
λ :{
| data Vector a b where
|     Vector :: a -> b -> Vector a b
|     T1 :: Int -> b -> T1 b
| type T1 = Vector Int
| :}
λ :t T1
T1 :: Int -> b -> T1 b

Answer 3

There is already a constructor for T1, and it is named Vector:

*Main> :t Vector :: Int -> b -> T1 b
Vector :: Int -> b -> T1 b :: Int -> b -> T1 b