Is there any way to do this?

type V = VList
{- type V2 a = V (V a)
type V4 a = V2 (V2 a)
type V8 a = V4 (V4 a)
type V16 a = V8 (V8 a)
type V32 a = V16 (V16 a) -}
type C a b c = a (b c)
type D a b = a b b
type E = D C
type V2 a = V (V a)
type V4 = E V2
type V8 = E V4
type V16 = E V8
type V32 = E V16

I want to make this type for example

type Vector25 = C (C V16 V8) V Empty

Without having to do

type Vector25 = (V16 (V8 (V Empty))

Is there any way to do this?

type V = VList
{- type V2 a = V (V a)
type V4 a = V2 (V2 a)
type V8 a = V4 (V4 a)
type V16 a = V8 (V8 a)
type V32 a = V16 (V16 a) -}
type C a b c = a (b c)
type D a b = a b b
type E = D C
type V2 a = V (V a)
type V4 = E V2
type V8 = E V4
type V16 = E V8
type V32 = E V16

I want to make this type for example

type Vector25 = C (C V16 V8) V Empty

Without having to do

type Vector25 = (V16 (V8 (V Empty))

• haskell
• types

• 1 Type synonyms must be fully applied, but there is Compose and Join. – Naïm Favier Commented 2 days ago
• Got it, so is there any easy way to do Vector25 or something of that ilk? – user28080356 Commented 2 days ago
• 1 By far the easiest way is to write V 25 times. You might also be able to do something with type-level natural numbers and GADTs, with a constructor like Wrap :: V (V' n) → V' ('S n) or something. – Naïm Favier Commented 2 days ago
• Writing it is better? I thought that even (V16 (V8 (V Empty))) would be much better. – user28080356 Commented 2 days ago

1 Answer 1

The following module loads into ghci just fine:

{-# LANGUAGE LiberalTypeSynonyms #-}
type V = []
type C a b c = a (b c)
type D a b = a b b
type E f a = D C f a
type V2 a = V (V a)
type V4 a = E V2 a
type V8 a = E V4 a
type V16 a = E V8 a
type V32 a = E V16 a
type Vector25 a = C (C V16 V8) V a

All the definitions are the same as yours, but eta-expanded. If you :k! it enough, it even reduces.

> :set -XLiberalTypeSynonyms
> :k! Vector25 Int
Vector25 Int :: *
= C V16 V8 [Int]
> :k! C V16 V8 [Int]
C V16 V8 [Int] :: *
= V16 (V8 [Int])
> :k! V16 (V8 [Int])
V16 (V8 [Int]) :: *
= C V8 V8 (C V4 V4 [Int])
> :k! C V8 V8 (C V4 V4 [Int])
C V8 V8 (C V4 V4 [Int]) :: *
= V8 (V8 (V4 (V4 [Int])))
> :k! V8 (V8 (V4 (V4 [Int])))
V8 (V8 (V4 (V4 [Int]))) :: *
= C V4 V4 (C V4 V4 (C V2 V2 (C V2 V2 [Int])))
> :k! C V4 V4 (C V4 V4 (C V2 V2 (C V2 V2 [Int])))
C V4 V4 (C V4 V4 (C V2 V2 (C V2 V2 [Int]))) :: *
= V4 (V4 (V4 (V4 (V2 (V2 (V2 (V2 [Int])))))))
> :k! V4 (V4 (V4 (V4 (V2 (V2 (V2 (V2 [Int])))))))
V4 (V4 (V4 (V4 (V2 (V2 (V2 (V2 [Int]))))))) :: *
= C V2 V2 (C V2 V2 (C V2 V2 (C V2 V2 [[[[[[[[[Int]]]]]]]]])))
> :k! C V2 V2 (C V2 V2 (C V2 V2 (C V2 V2 [[[[[[[[[Int]]]]]]]]])))
C V2 V2 (C V2 V2 (C V2 V2 (C V2 V2 [[[[[[[[[Int]]]]]]]]]))) :: *
= V2 (V2 (V2 (V2 (V2 (V2 (V2 (V2 [[[[[[[[[Int]]]]]]]]])))))))
> :k! V2 (V2 (V2 (V2 (V2 (V2 (V2 (V2 [[[[[[[[[Int]]]]]]]]])))))))
V2 (V2 (V2 (V2 (V2 (V2 (V2 (V2 [[[[[[[[[Int]]]]]]]]]))))))) :: *
= [[[[[[[[[[[[[[[[[[[[[[[[[Int]]]]]]]]]]]]]]]]]]]]]]]]]

I'm not sure why it doesn't reduce fully at the very first query. Perhaps it's a bug.

I'll also note this:

> length "[[[[[[[[[[[[[[[[[[[[[[[[[Int]]]]]]]]]]]]]]]]]]]]]]]]]"
53
> length "{-# LANGUAGE LiberalTypeSynonyms #-} type V = [] type C a b c = a (b c) type D a b = a b b type E f a = D C f a type V2 a = V (V a) type V4 a = E V2 a type V8 a = E V4 a type V16 a = E V8 a type V32 a = E V16 a type Vector25 a = C (C V16 V8) V a"
245