CODEWITHSUNDEEP
haskelltypes
user28080356
user28080356

Reputation: 71

Is there a type composition operator in Haskell?

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))

Upvotes: 2

Views: 98

Answers (2)

K. A. Buhr
K. A. Buhr

Reputation: 51119

As an alternative approach for this specific problem, you can define a recursive type family using type level natural numbers:

type family Vec n a where
  Vec 0 a = a
  Vec n a = Vec (n-1) (V a)

It requires a few extensions and a module, but after loading the following example into GHCi:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module V25 where

import GHC.TypeNats

data V a = V a

type family Vec n a where
  Vec 0 a = a
  Vec n a = Vec (n-1) (V a)

you can do the following at the GHCi prompt:

λ> :kind! Vec 25 Int
Vec 25 Int :: *
= V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V (V Int))))))))))))))))))))))))

Upvotes: 2

Daniel Wagner
Daniel Wagner

Reputation: 153172

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

Upvotes: 2

Related Questions