public
Created

more type lit woe

  • 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 57 58 59 60
{-# 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::Nat) <= (a::Nat), (b + d) ~ a) => AbsDiff a b d where
 
 
 
 
--this doesn't type check
a ::( AbsDiff (2::Nat) (1::Nat) (d:: Nat ), SingI d)=> Sing d
a = sing
 
 
{-#
*Data.TypeLits.GCD> :t a
 
<interactive>:1:1:
Could not deduce (1 <= 2) arising from a use of `a'
from the context (SingI Nat d, (1 + d) ~ 2)
bound by the inferred type of
it :: (SingI Nat d, (1 + d) ~ 2) => Sing Nat d
at Top level
Possible fix: add an instance declaration for (1 <= 2)
In the expression: a
*Data.TypeLits.GCD>
 
#-}

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.