Dependent Types in Haskell

user_12314961 0
Viewed 158

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?

haskell
1 Answers

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.

user_152075680
Related