Skip to content

Instantly share code, notes, and snippets.

@aljce
Last active April 13, 2018 23:26
Show Gist options
  • Save aljce/299606a6b3328f4360d230eb05198192 to your computer and use it in GitHub Desktop.
Save aljce/299606a6b3328f4360d230eb05198192 to your computer and use it in GitHub Desktop.
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module Pokemon where
import Data.Kind (Type)
import Data.Void (Void)
import Type.Reflection ((:~:)(..))
data PokemonType = None | Fire | Water | Grass
data Pokemon (a :: PokemonType) (b :: PokemonType) where
Poke :: (a :~: b -> Void) -> Pokemon a b
bulbasaur :: Pokemon Grass None
bulbasaur= Poke (\case {})
@glguy
Copy link

glguy commented Apr 13, 2018

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
module Demo where

import Data.Kind (Type, Constraint)
import Data.Void (Void)
import Type.Reflection ((:~:)(..))

data PokemonType = None | Fire | Water | Grass

type family Different a b :: Constraint where
  Different a a = () ~ Int
  Different a b = ()

data Pokemon (a :: PokemonType) (b :: PokemonType) where
  Poke :: Different a b => Pokemon a b

charmander :: Pokemon Fire None
charmander = Poke

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment