CODEWITHSUNDEEP
haskell
kingZthefirst
kingZthefirst

Reputation: 11

Dependent Types in Haskell

The following does not work in Haskell-

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances,
             RankNTypes, PolyKinds #-}

import Data.Kind

data Payload :: (f :: a -> Type) -> (e :: a) -> Type where
  MkPayload :: (e :: a) -> (t :: f e) -> Payload f e

payload :: Payload f e -> f e
payload (MkPayload e t) = t

    • Expecting one more argument to ‘f :: a -> Type’
      Expected a type, but ‘f :: a -> Type’ has kind ‘a -> Type’
    • In the kind ‘(f :: a -> Type) -> (e :: a) -> Type’
      In the data type declaration for ‘Payload’
  |
6 | data Payload :: (f :: a -> Type) -> (e :: a) -> Type where
  |                  ^^^^^^^^^^^^^^

Is there any other way someone can define dependent types in Haskell?

Upvotes: 1

Views: 456

Answers (1)

Noughtmare
Noughtmare

Reputation: 10645

You cannot use that _ :: _ notation in types as you might be used to from Agda. Instead just leave the names out and just write the types:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances,
             RankNTypes, PolyKinds #-}

import Data.Kind ( Type )

data Payload :: (a -> Type) -> a -> Type where
  MkPayload :: a -> f e -> Payload f e

payload :: Payload f e -> f e
payload (MkPayload e t) = t

That CUSK (complete user specified kind) notation is discouraged, instead you should use standalone kind signatures:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances,
             RankNTypes, PolyKinds, StandaloneKindSignatures #-}

import Data.Kind ( Type )

type Payload :: (a -> Type) -> a -> Type
data Payload f e where
  MkPayload :: a -> f e -> Payload f e

payload :: Payload f e -> f e
payload (MkPayload e t) = t

Leaving out the names does mean you lose some expressivity, but that isn't required for this example. There are techniques to recover most of that expressivity such as singletons that David Young mentioned.

Upvotes: 3

Related Questions