public
Created

type lit example problem 1

  • Download Gist
gistfile1.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
{-# LANGUAGE DataKinds #-} -- to declare the kinds
{-# LANGUAGE KindSignatures #-} -- (used all over)
{-# LANGUAGE TypeFamilies #-} -- for declaring operators + sing family
{-# LANGUAGE TypeOperators #-} -- for declaring operator
{-# LANGUAGE EmptyDataDecls #-} -- for declaring the kinds
{-# LANGUAGE GADTs #-} -- for examining type nats
{-# LANGUAGE PolyKinds #-} -- for Sing family
{-# LANGUAGE UndecidableInstances #-} -- for a bunch of the instances
{-# LANGUAGE FlexibleInstances #-} -- for kind parameters
{-# LANGUAGE FlexibleContexts #-} -- for kind parameters
{-# LANGUAGE ScopedTypeVariables #-} -- for kind parameters\
{-# LANGUAGE MultiParamTypeClasses #-} -- for <=, singRep, SingE
{-# LANGUAGE FunctionalDependencies #-} -- for SingRep and SingE
 
 
 
 
{-# OPTIONS_GHC -XNoImplicitPrelude #-}
 
 
 
 
module Data.TypeLits.GCD where
 
import GHC.TypeLits
--import GHC.Num(Integer, (-))
 
 
--class EqNat (a:: Nat) (b :: Nat) where
 
--instance (SingI a, SingI b, a <= b, b<= a) => EqNat a b where
 
 
class AbsDiff (a::Nat) (b::Nat) (d::Nat) | a b -> d where
 
instance (SingI a,SingI b, SingI d, (b + d) ~ a) => AbsDiff a b d where
 
 
 
 
--this doesn't type check
a ::( AbsDiff 2 1 (d:: Nat ), SingI Nat, (1+d)~ 2)=> Sing d
a = sing
 
 
{- Data/TypeLits/GCD.hs:44:5:
Could not deduce (SingI Nat d) arising from a use of `sing'
from the context (AbsDiff 2 1 d, SingI * Nat, (1 + d) ~ 2)
bound by the type signature for
a :: (AbsDiff 2 1 d, SingI * Nat, (1 + d) ~ 2) => Sing Nat d
at Data/TypeLits/GCD.hs:43:5-59
Possible fix: add an instance declaration for (SingI Nat d)
In the expression: sing
In an equation for `a': a = sing
Failed, modules loaded: none. -}

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.